set V = the carrier of G1 \/ the carrier of G2;
set E = the carrier' of G1 \/ the carrier' of G2;
A3: ex S being Function of (the carrier' of G1 \/ the carrier' of G2),(the carrier of G1 \/ the carrier of G2) st
( ( for v being set st v in the carrier' of G1 holds
S . v = the Source of G1 . v ) & ( for v being set st v in the carrier' of G2 holds
S . v = the Source of G2 . v ) )

proof

defpred S₁[ set , set ] means ( ( $1 in the carrier' of G1 implies $2 = the Source of G1 . $1 ) & ( $1 in the carrier' of G2 implies $2 = the Source of G2 . $1 ) );
A4: for x being set st x in the carrier' of G1 \/ the carrier' of G2 holds
ex y being set st
( y in the carrier of G1 \/ the carrier of G2 & S₁[x,y] )

proof

let x be set ; :: thesis: ( x in the carrier' of G1 \/ the carrier' of G2 implies ex y being set st
( y in the carrier of G1 \/ the carrier of G2 & S₁[x,y] ) )
assume A5: x in the carrier' of G1 \/ the carrier' of G2 ; :: thesis: ex y being set st
( y in the carrier of G1 \/ the carrier of G2 & S₁[x,y] )
A6: ( x in the carrier' of G1 implies ex y being set st
( y in the carrier of G1 \/ the carrier of G2 & S₁[x,y] ) )

proof

assume A7: x in the carrier' of G1 ; :: thesis: ex y being set st
( y in the carrier of G1 \/ the carrier of G2 & S₁[x,y] )
take y = the Source of G1 . x; :: thesis: ( y in the carrier of G1 \/ the carrier of G2 & S₁[x,y] )
A8: y in the carrier of G1 by A7, FUNCT_2:7;
thus y in the carrier of G1 \/ the carrier of G2 by A8, XBOOLE_0:def 3; :: thesis: S₁[x,y]
thus ( x in the carrier' of G1 implies y = the Source of G1 . x ) ; :: thesis: ( x in the carrier' of G2 implies y = the Source of G2 . x )
assume A9: x in the carrier' of G2 ; :: thesis: y = the Source of G2 . x
A10: x in the carrier' of G1 /\ the carrier' of G2 by A7, A9, XBOOLE_0:def 4;
A11: dom the Source of G1 = the carrier' of G1 by FUNCT_2:def 1;
A12: x in (dom the Source of G1) /\ (dom the Source of G2) by A10, A11, FUNCT_2:def 1;
thus y = the Source of G2 . x by A1, A12, PARTFUN1:def 6; :: thesis: verum

end;

A13: ( not x in the carrier' of G1 implies ex y being set st
( y in the carrier of G1 \/ the carrier of G2 & S₁[x,y] ) )

proof

assume A14: not x in the carrier' of G1 ; :: thesis: ex y being set st
( y in the carrier of G1 \/ the carrier of G2 & S₁[x,y] )
A15: x in the carrier' of G2 by A5, A14, XBOOLE_0:def 3;
take y = the Source of G2 . x; :: thesis: ( y in the carrier of G1 \/ the carrier of G2 & S₁[x,y] )
A16: y in the carrier of G2 by A15, FUNCT_2:7;
thus y in the carrier of G1 \/ the carrier of G2 by A16, XBOOLE_0:def 3; :: thesis: S₁[x,y]
thus S₁[x,y] by A14; :: thesis: verum

end;

thus ex y being set st
( y in the carrier of G1 \/ the carrier of G2 & S₁[x,y] ) by A6, A13; :: thesis: verum

end;

consider S being Function of (the carrier' of G1 \/ the carrier' of G2),(the carrier of G1 \/ the carrier of G2) such that
A17: for x being set st x in the carrier' of G1 \/ the carrier' of G2 holds
S₁[x,S . x] from FUNCT_2:sch 1(A4);
take S ; :: thesis: ( ( for v being set st v in the carrier' of G1 holds
S . v = the Source of G1 . v ) & ( for v being set st v in the carrier' of G2 holds
S . v = the Source of G2 . v ) )
thus for v being set st v in the carrier' of G1 holds
S . v = the Source of G1 . v :: thesis: for v being set st v in the carrier' of G2 holds
S . v = the Source of G2 . v

proof

let v be set ; :: thesis: ( v in the carrier' of G1 implies S . v = the Source of G1 . v )
assume A18: v in the carrier' of G1 ; :: thesis: S . v = the Source of G1 . v
A19: v in the carrier' of G1 \/ the carrier' of G2 by A18, XBOOLE_0:def 3;
thus S . v = the Source of G1 . v by A17, A18, A19; :: thesis: verum

end;

let v be set ; :: thesis: ( v in the carrier' of G2 implies S . v = the Source of G2 . v )
assume A20: v in the carrier' of G2 ; :: thesis: S . v = the Source of G2 . v
A21: v in the carrier' of G1 \/ the carrier' of G2 by A20, XBOOLE_0:def 3;
thus S . v = the Source of G2 . v by A17, A20, A21; :: thesis: verum

end;

consider S being Function of (the carrier' of G1 \/ the carrier' of G2),(the carrier of G1 \/ the carrier of G2) such that
A22: for v being set st v in the carrier' of G1 holds
S . v = the Source of G1 . v and
A23: for v being set st v in the carrier' of G2 holds
S . v = the Source of G2 . v by A3;
A24: ex T being Function of (the carrier' of G1 \/ the carrier' of G2),(the carrier of G1 \/ the carrier of G2) st
( ( for v being set st v in the carrier' of G1 holds
T . v = the Target of G1 . v ) & ( for v being set st v in the carrier' of G2 holds
T . v = the Target of G2 . v ) )

proof

defpred S₁[ set , set ] means ( ( $1 in the carrier' of G1 implies $2 = the Target of G1 . $1 ) & ( $1 in the carrier' of G2 implies $2 = the Target of G2 . $1 ) );
A25: for x being set st x in the carrier' of G1 \/ the carrier' of G2 holds
ex y being set st
( y in the carrier of G1 \/ the carrier of G2 & S₁[x,y] )

proof

let x be set ; :: thesis: ( x in the carrier' of G1 \/ the carrier' of G2 implies ex y being set st
( y in the carrier of G1 \/ the carrier of G2 & S₁[x,y] ) )
assume A26: x in the carrier' of G1 \/ the carrier' of G2 ; :: thesis: ex y being set st
( y in the carrier of G1 \/ the carrier of G2 & S₁[x,y] )
A27: ( x in the carrier' of G1 implies ex y being set st
( y in the carrier of G1 \/ the carrier of G2 & S₁[x,y] ) )

proof

assume A28: x in the carrier' of G1 ; :: thesis: ex y being set st
( y in the carrier of G1 \/ the carrier of G2 & S₁[x,y] )
take y = the Target of G1 . x; :: thesis: ( y in the carrier of G1 \/ the carrier of G2 & S₁[x,y] )
A29: y in the carrier of G1 by A28, FUNCT_2:7;
thus y in the carrier of G1 \/ the carrier of G2 by A29, XBOOLE_0:def 3; :: thesis: S₁[x,y]
thus ( x in the carrier' of G1 implies y = the Target of G1 . x ) ; :: thesis: ( x in the carrier' of G2 implies y = the Target of G2 . x )
assume A30: x in the carrier' of G2 ; :: thesis: y = the Target of G2 . x
A31: x in the carrier' of G1 /\ the carrier' of G2 by A28, A30, XBOOLE_0:def 4;
A32: dom the Target of G1 = the carrier' of G1 by FUNCT_2:def 1;
A33: x in (dom the Target of G1) /\ (dom the Target of G2) by A31, A32, FUNCT_2:def 1;
thus y = the Target of G2 . x by A2, A33, PARTFUN1:def 6; :: thesis: verum

end;

A34: ( not x in the carrier' of G1 implies ex y being set st
( y in the carrier of G1 \/ the carrier of G2 & S₁[x,y] ) )

proof

assume A35: not x in the carrier' of G1 ; :: thesis: ex y being set st
( y in the carrier of G1 \/ the carrier of G2 & S₁[x,y] )
A36: x in the carrier' of G2 by A26, A35, XBOOLE_0:def 3;
take y = the Target of G2 . x; :: thesis: ( y in the carrier of G1 \/ the carrier of G2 & S₁[x,y] )
A37: y in the carrier of G2 by A36, FUNCT_2:7;
thus y in the carrier of G1 \/ the carrier of G2 by A37, XBOOLE_0:def 3; :: thesis: S₁[x,y]
thus S₁[x,y] by A35; :: thesis: verum

end;

thus ex y being set st
( y in the carrier of G1 \/ the carrier of G2 & S₁[x,y] ) by A27, A34; :: thesis: verum

end;

consider S being Function of (the carrier' of G1 \/ the carrier' of G2),(the carrier of G1 \/ the carrier of G2) such that
A38: for x being set st x in the carrier' of G1 \/ the carrier' of G2 holds
S₁[x,S . x] from FUNCT_2:sch 1(A25);
take S ; :: thesis: ( ( for v being set st v in the carrier' of G1 holds
S . v = the Target of G1 . v ) & ( for v being set st v in the carrier' of G2 holds
S . v = the Target of G2 . v ) )
thus for v being set st v in the carrier' of G1 holds
S . v = the Target of G1 . v :: thesis: for v being set st v in the carrier' of G2 holds
S . v = the Target of G2 . v

proof

let v be set ; :: thesis: ( v in the carrier' of G1 implies S . v = the Target of G1 . v )
assume A39: v in the carrier' of G1 ; :: thesis: S . v = the Target of G1 . v
A40: v in the carrier' of G1 \/ the carrier' of G2 by A39, XBOOLE_0:def 3;
thus S . v = the Target of G1 . v by A38, A39, A40; :: thesis: verum

end;

let v be set ; :: thesis: ( v in the carrier' of G2 implies S . v = the Target of G2 . v )
assume A41: v in the carrier' of G2 ; :: thesis: S . v = the Target of G2 . v
A42: v in the carrier' of G1 \/ the carrier' of G2 by A41, XBOOLE_0:def 3;
thus S . v = the Target of G2 . v by A38, A41, A42; :: thesis: verum

end;

consider T being Function of (the carrier' of G1 \/ the carrier' of G2),(the carrier of G1 \/ the carrier of G2) such that
A43: for v being set st v in the carrier' of G1 holds
T . v = the Target of G1 . v and
A44: for v being set st v in the carrier' of G2 holds
T . v = the Target of G2 . v by A24;
reconsider G = MultiGraphStruct(# (the carrier of G1 \/ the carrier of G2),(the carrier' of G1 \/ the carrier' of G2),S,T #) as strict Graph ;
take G ; :: thesis: ( the carrier of G = the carrier of G1 \/ the carrier of G2 & the carrier' of G = the carrier' of G1 \/ the carrier' of G2 & ( for v being set st v in the carrier' of G1 holds
( the Source of G . v = the Source of G1 . v & the Target of G . v = the Target of G1 . v ) ) & ( for v being set st v in the carrier' of G2 holds
( the Source of G . v = the Source of G2 . v & the Target of G . v = the Target of G2 . v ) ) )
thus the carrier of G = the carrier of G1 \/ the carrier of G2 ; :: thesis: ( the carrier' of G = the carrier' of G1 \/ the carrier' of G2 & ( for v being set st v in the carrier' of G1 holds
( the Source of G . v = the Source of G1 . v & the Target of G . v = the Target of G1 . v ) ) & ( for v being set st v in the carrier' of G2 holds
( the Source of G . v = the Source of G2 . v & the Target of G . v = the Target of G2 . v ) ) )
thus the carrier' of G = the carrier' of G1 \/ the carrier' of G2 ; :: thesis: ( ( for v being set st v in the carrier' of G1 holds
( the Source of G . v = the Source of G1 . v & the Target of G . v = the Target of G1 . v ) ) & ( for v being set st v in the carrier' of G2 holds
( the Source of G . v = the Source of G2 . v & the Target of G . v = the Target of G2 . v ) ) )
thus for v being set st v in the carrier' of G1 holds
( the Source of G . v = the Source of G1 . v & the Target of G . v = the Target of G1 . v ) by A22, A43; :: thesis: for v being set st v in the carrier' of G2 holds
( the Source of G . v = the Source of G2 . v & the Target of G . v = the Target of G2 . v )
let v be set ; :: thesis: ( v in the carrier' of G2 implies ( the Source of G . v = the Source of G2 . v & the Target of G . v = the Target of G2 . v ) )
assume A45: v in the carrier' of G2 ; :: thesis: ( the Source of G . v = the Source of G2 . v & the Target of G . v = the Target of G2 . v )
thus the Source of G . v = the Source of G2 . v by A23, A45; :: thesis: the Target of G . v = the Target of G2 . v
thus the Target of G . v = the Target of G2 . v by A44, A45; :: thesis: verum