In this article the sum (or disjoint union) of graphs is formalized in the Mizar system [4], [1], based on the formalization of graphs in [9].