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
A2: the carrier of (G1 \/ G2) = the carrier of G2 \/ the carrier of G1 by A1, Def3
.= the carrier of (G2 \/ G1) by A1, Def3 ;
A3: the carrier' of (G1 \/ G2) = the carrier' of G2 \/ the carrier' of G1 by A1, Def3
.= the carrier' of (G2 \/ G1) by A1, Def3 ;
A4: dom the Source of (G1 \/ G2) = the carrier' of (G2 \/ G1) by A3, FUNCT_2:def 1
.= dom the Source of (G2 \/ G1) by FUNCT_2:def 1 ;
A5: for v being set 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 set ; :: thesis: ( v in dom the Source of (G1 \/ G2) implies the Source of (G1 \/ G2) . v = the Source of (G2 \/ G1) . v )
assume A6: v in dom the Source of (G1 \/ G2) ; :: thesis: the Source of (G1 \/ G2) . v = the Source of (G2 \/ G1) . v
A7: v in the carrier' of (G1 \/ G2) by A6;
A8: v in the carrier' of G1 \/ the carrier' of G2 by A1, A7, Def3;

A9: now

assume A10: v in the carrier' of G1 ; :: thesis: the Source of (G1 \/ G2) . v = the Source of (G2 \/ G1) . v
thus the Source of (G1 \/ G2) . v = the Source of G1 . v by A1, A10, Def3
.= the Source of (G2 \/ G1) . v by A1, A10, Def3 ; :: thesis: verum

end;

A11: now

assume A12: v in the carrier' of G2 ; :: thesis: the Source of (G1 \/ G2) . v = the Source of (G2 \/ G1) . v
thus the Source of (G1 \/ G2) . v = the Source of G2 . v by A1, A12, Def3
.= the Source of (G2 \/ G1) . v by A1, A12, Def3 ; :: thesis: verum

end;

thus the Source of (G1 \/ G2) . v = the Source of (G2 \/ G1) . v by A8, A9, A11, XBOOLE_0:def 3; :: thesis: verum

end;

A13: the Source of (G1 \/ G2) = the Source of (G2 \/ G1) by A4, A5, FUNCT_1:9;
A14: 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 ;
A15: for v being set 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 set ; :: thesis: ( v in dom the Target of (G1 \/ G2) implies the Target of (G1 \/ G2) . v = the Target of (G2 \/ G1) . v )
assume A16: v in dom the Target of (G1 \/ G2) ; :: thesis: the Target of (G1 \/ G2) . v = the Target of (G2 \/ G1) . v
A17: v in the carrier' of (G1 \/ G2) by A16;
A18: v in the carrier' of G1 \/ the carrier' of G2 by A1, A17, Def3;

A19: now

assume A20: v in the carrier' of G1 ; :: thesis: the Target of (G1 \/ G2) . v = the Target of (G2 \/ G1) . v
thus the Target of (G1 \/ G2) . v = the Target of G1 . v by A1, A20, Def3
.= the Target of (G2 \/ G1) . v by A1, A20, Def3 ; :: thesis: verum

end;

A21: now

assume A22: v in the carrier' of G2 ; :: thesis: the Target of (G1 \/ G2) . v = the Target of (G2 \/ G1) . v
thus the Target of (G1 \/ G2) . v = the Target of G2 . v by A1, A22, Def3
.= the Target of (G2 \/ G1) . v by A1, A22, Def3 ; :: thesis: verum

end;

thus the Target of (G1 \/ G2) . v = the Target of (G2 \/ G1) . v by A18, A19, A21, XBOOLE_0:def 3; :: thesis: verum

end;

thus G1 \/ G2 = G2 \/ G1 by A2, A3, A13, A14, A15, FUNCT_1:9; :: thesis: verum