set V = the carrier of G1 \/ the carrier of G2;
set E = the carrier' of G1 \/ the carrier' of G2;
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] )
y in the carrier of G1 by A7, FUNCT_2:7;
hence y in the carrier of G1 \/ the carrier of G2 by 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 x in the carrier' of G2 ; :: thesis: y = the Source of G2 . x
then A10: x in the carrier' of G1 /\ the carrier' of G2 by A7, XBOOLE_0:def 4;
dom the Source of G1 = the carrier' of G1 by FUNCT_2:def 1;
then x in (dom the Source of G1) /\ (dom the Source of G2) by A10, FUNCT_2:def 1;
hence y = the Source of G2 . x by A1, PARTFUN1:def 6; :: thesis: verum

end;

( 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] )
then A15: x in the carrier' of G2 by A5, 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] )
y in the carrier of G2 by A15, FUNCT_2:7;
hence y in the carrier of G1 \/ the carrier of G2 by XBOOLE_0:def 3; :: thesis: S₁[x,y]
thus S₁[x,y] by A14; :: thesis: verum

end;

hence ex y being set st
( y in the carrier of G1 \/ the carrier of G2 & S₁[x,y] ) by A6; :: 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
then v in the carrier' of G1 \/ the carrier' of G2 by XBOOLE_0:def 3;
hence S . v = the Source of G1 . v by A17, A18; :: 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
then v in the carrier' of G1 \/ the carrier' of G2 by XBOOLE_0:def 3;
hence S . v = the Source of G2 . v by A17, A20; :: thesis: verum

end;

then 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 ;
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] )
y in the carrier of G1 by A28, FUNCT_2:7;
hence y in the carrier of G1 \/ the carrier of G2 by 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 x in the carrier' of G2 ; :: thesis: y = the Target of G2 . x
then A31: x in the carrier' of G1 /\ the carrier' of G2 by A28, XBOOLE_0:def 4;
dom the Target of G1 = the carrier' of G1 by FUNCT_2:def 1;
then x in (dom the Target of G1) /\ (dom the Target of G2) by A31, FUNCT_2:def 1;
hence y = the Target of G2 . x by A2, PARTFUN1:def 6; :: thesis: verum

end;

( 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] )
then A36: x in the carrier' of G2 by A26, 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] )
y in the carrier of G2 by A36, FUNCT_2:7;
hence y in the carrier of G1 \/ the carrier of G2 by XBOOLE_0:def 3; :: thesis: S₁[x,y]
thus S₁[x,y] by A35; :: thesis: verum

end;

hence ex y being set st
( y in the carrier of G1 \/ the carrier of G2 & S₁[x,y] ) by A27; :: 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
then v in the carrier' of G1 \/ the carrier' of G2 by XBOOLE_0:def 3;
hence S . v = the Target of G1 . v by A38, A39; :: 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
then v in the carrier' of G1 \/ the carrier' of G2 by XBOOLE_0:def 3;
hence S . v = the Target of G2 . v by A38, A41; :: thesis: verum

end;

then 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 ;
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 )
hence the Source of G . v = the Source of G2 . v by A23; :: 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