let G be strict Graph; :: thesis: G = G \/ G
A1: the carrier of (G \/ G) = the carrier of G \/ the carrier of G by Def5
.= the carrier of G ;
A2: the carrier' of (G \/ G) = the carrier' of G \/ the carrier' of G by Def5
.= the carrier' of G ;
then A3: dom the Source of G = the carrier' of (G \/ G) by FUNCT_2:def 1
.= dom the Source of (G \/ G) by FUNCT_2:def 1 ;
for v being object st v in dom the Source of G holds
the Source of G . v = the Source of (G \/ G) . v by Def5;
then A4: the Source of G = the Source of (G \/ G) by A3;
A5: dom the Target of G = the carrier' of (G \/ G) by A2, FUNCT_2:def 1
.= dom the Target of (G \/ G) by FUNCT_2:def 1 ;
for v being object st v in dom the Target of G holds
the Target of G . v = the Target of (G \/ G) . v by Def5;
hence G = G \/ G by A1, A2, A4, A5, FUNCT_1:2; :: thesis: verum