let G be strict Graph; 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; verum