let G1, G2 be Graph; :: thesis: ( the Source of G1 tolerates the Source of G2 & the Target of G1 tolerates the Target of G2 implies G1 \/ G2 = G2 \/ G1 )
assume A1: ( the Source of G1 tolerates the Source of G2 & the Target of G1 tolerates the Target of G2 ) ; :: thesis: G1 \/ G2 = G2 \/ G1
then A2: the carrier of (G1 \/ G2) = the carrier of G2 \/ the carrier of G1 by Def5
.= the carrier of (G2 \/ G1) by A1, Def5 ;
A3: the carrier' of (G1 \/ G2) = the carrier' of G2 \/ the carrier' of G1 by A1, Def5
.= the carrier' of (G2 \/ G1) by A1, Def5 ;
then A4: dom the Source of (G1 \/ G2) = the carrier' of (G2 \/ G1) by FUNCT_2:def 1
.= dom the Source of (G2 \/ G1) by FUNCT_2:def 1 ;
for v being object st v in dom the Source of (G1 \/ G2) holds
the Source of (G1 \/ G2) . v = the Source of (G2 \/ G1) . v
proof
let v be object ; :: thesis: ( v in dom the Source of (G1 \/ G2) implies the Source of (G1 \/ G2) . v = the Source of (G2 \/ G1) . v )
assume v in dom the Source of (G1 \/ G2) ; :: thesis: the Source of (G1 \/ G2) . v = the Source of (G2 \/ G1) . v
then v in the carrier' of (G1 \/ G2) ;
then A5: v in the carrier' of G1 \/ the carrier' of G2 by A1, Def5;
A6: now :: thesis: ( v in the carrier' of G1 implies the Source of (G1 \/ G2) . v = the Source of (G2 \/ G1) . v )
assume A7: v in the carrier' of G1 ; :: thesis: the Source of (G1 \/ G2) . v = the Source of (G2 \/ G1) . v
hence the Source of (G1 \/ G2) . v = the Source of G1 . v by A1, Def5
.= the Source of (G2 \/ G1) . v by A1, A7, Def5 ;
:: thesis: verum
end;
now :: thesis: ( v in the carrier' of G2 implies the Source of (G1 \/ G2) . v = the Source of (G2 \/ G1) . v )
assume A8: v in the carrier' of G2 ; :: thesis: the Source of (G1 \/ G2) . v = the Source of (G2 \/ G1) . v
hence the Source of (G1 \/ G2) . v = the Source of G2 . v by A1, Def5
.= the Source of (G2 \/ G1) . v by A1, A8, Def5 ;
:: thesis: verum
end;
hence the Source of (G1 \/ G2) . v = the Source of (G2 \/ G1) . v by A5, A6, XBOOLE_0:def 3; :: thesis: verum
end;
then A9: the Source of (G1 \/ G2) = the Source of (G2 \/ G1) by A4;
A10: dom the Target of (G1 \/ G2) = the carrier' of (G2 \/ G1) by A3, FUNCT_2:def 1
.= dom the Target of (G2 \/ G1) by FUNCT_2:def 1 ;
for v being object st v in dom the Target of (G1 \/ G2) holds
the Target of (G1 \/ G2) . v = the Target of (G2 \/ G1) . v
proof
let v be object ; :: thesis: ( v in dom the Target of (G1 \/ G2) implies the Target of (G1 \/ G2) . v = the Target of (G2 \/ G1) . v )
assume v in dom the Target of (G1 \/ G2) ; :: thesis: the Target of (G1 \/ G2) . v = the Target of (G2 \/ G1) . v
then v in the carrier' of (G1 \/ G2) ;
then A11: v in the carrier' of G1 \/ the carrier' of G2 by A1, Def5;
A12: now :: thesis: ( v in the carrier' of G1 implies the Target of (G1 \/ G2) . v = the Target of (G2 \/ G1) . v )
assume A13: v in the carrier' of G1 ; :: thesis: the Target of (G1 \/ G2) . v = the Target of (G2 \/ G1) . v
hence the Target of (G1 \/ G2) . v = the Target of G1 . v by A1, Def5
.= the Target of (G2 \/ G1) . v by A1, A13, Def5 ;
:: thesis: verum
end;
now :: thesis: ( v in the carrier' of G2 implies the Target of (G1 \/ G2) . v = the Target of (G2 \/ G1) . v )
assume A14: v in the carrier' of G2 ; :: thesis: the Target of (G1 \/ G2) . v = the Target of (G2 \/ G1) . v
hence the Target of (G1 \/ G2) . v = the Target of G2 . v by A1, Def5
.= the Target of (G2 \/ G1) . v by A1, A14, Def5 ;
:: thesis: verum
end;
hence the Target of (G1 \/ G2) . v = the Target of (G2 \/ G1) . v by A11, A12, XBOOLE_0:def 3; :: thesis: verum
end;
hence G1 \/ G2 = G2 \/ G1 by A2, A3, A9, A10, FUNCT_1:2; :: thesis: verum