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 S1[ object , object ] 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 ) );
A3: for x being object st x in the carrier' of G1 \/ the carrier' of G2 holds
ex y being object st
( y in the carrier of G1 \/ the carrier of G2 & S1[x,y] )
proof
let x be object ; :: thesis: ( x in the carrier' of G1 \/ the carrier' of G2 implies ex y being object st
( y in the carrier of G1 \/ the carrier of G2 & S1[x,y] ) )
assume A4: x in the carrier' of G1 \/ the carrier' of G2 ; :: thesis: ex y being object st
( y in the carrier of G1 \/ the carrier of G2 & S1[x,y] )
A5: ( x in the carrier' of G1 implies ex y being object st
( y in the carrier of G1 \/ the carrier of G2 & S1[x,y] ) )
proof
assume A6: x in the carrier' of G1 ; :: thesis: ex y being object st
( y in the carrier of G1 \/ the carrier of G2 & S1[x,y] )
take y = the Source of G1 . x; :: thesis: ( y in the carrier of G1 \/ the carrier of G2 & S1[x,y] )
y in the carrier of G1 by A6, FUNCT_2:5;
hence y in the carrier of G1 \/ the carrier of G2 by XBOOLE_0:def 3; :: thesis: S1[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 A7: x in the carrier' of G1 /\ the carrier' of G2 by A6, 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 A7, FUNCT_2:def 1;
hence y = the Source of G2 . x by A1, PARTFUN1:def 4; :: thesis: verum
end;
( not x in the carrier' of G1 implies ex y being object st
( y in the carrier of G1 \/ the carrier of G2 & S1[x,y] ) )
proof
assume A8: not x in the carrier' of G1 ; :: thesis: ex y being object st
( y in the carrier of G1 \/ the carrier of G2 & S1[x,y] )
then A9: x in the carrier' of G2 by A4, XBOOLE_0:def 3;
take y = the Source of G2 . x; :: thesis: ( y in the carrier of G1 \/ the carrier of G2 & S1[x,y] )
y in the carrier of G2 by A9, FUNCT_2:5;
hence y in the carrier of G1 \/ the carrier of G2 by XBOOLE_0:def 3; :: thesis: S1[x,y]
thus S1[x,y] by A8; :: thesis: verum
end;
hence ex y being object st
( y in the carrier of G1 \/ the carrier of G2 & S1[x,y] ) by A5; :: 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
A10: for x being object st x in the carrier' of G1 \/ the carrier' of G2 holds
S1[x,S . x] from FUNCT_2:sch 1(A3);
 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 A11: 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 A10, A11; :: thesis: verum
end;
let v be set ; :: thesis: ( v in the carrier' of G2 implies S . v = the Source of G2 . v )
assume A12: 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 A10, A12; :: 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
A13: for v being set st v in the carrier' of G1 holds
S . v = the Source of G1 . v and
A14: 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 S1[ object , object ] 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 ) );
A15: for x being object st x in the carrier' of G1 \/ the carrier' of G2 holds
ex y being object st
( y in the carrier of G1 \/ the carrier of G2 & S1[x,y] )
proof
let x be object ; :: thesis: ( x in the carrier' of G1 \/ the carrier' of G2 implies ex y being object st
( y in the carrier of G1 \/ the carrier of G2 & S1[x,y] ) )
assume A16: x in the carrier' of G1 \/ the carrier' of G2 ; :: thesis: ex y being object st
( y in the carrier of G1 \/ the carrier of G2 & S1[x,y] )
A17: ( x in the carrier' of G1 implies ex y being object st
( y in the carrier of G1 \/ the carrier of G2 & S1[x,y] ) )
proof
assume A18: x in the carrier' of G1 ; :: thesis: ex y being object st
( y in the carrier of G1 \/ the carrier of G2 & S1[x,y] )
take y = the Target of G1 . x; :: thesis: ( y in the carrier of G1 \/ the carrier of G2 & S1[x,y] )
y in the carrier of G1 by A18, FUNCT_2:5;
hence y in the carrier of G1 \/ the carrier of G2 by XBOOLE_0:def 3; :: thesis: S1[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 A19: x in the carrier' of G1 /\ the carrier' of G2 by A18, 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 A19, FUNCT_2:def 1;
hence y = the Target of G2 . x by A2, PARTFUN1:def 4; :: thesis: verum
end;
( not x in the carrier' of G1 implies ex y being object st
( y in the carrier of G1 \/ the carrier of G2 & S1[x,y] ) )
proof
assume A20: not x in the carrier' of G1 ; :: thesis: ex y being object st
( y in the carrier of G1 \/ the carrier of G2 & S1[x,y] )
then A21: x in the carrier' of G2 by A16, XBOOLE_0:def 3;
take y = the Target of G2 . x; :: thesis: ( y in the carrier of G1 \/ the carrier of G2 & S1[x,y] )
y in the carrier of G2 by A21, FUNCT_2:5;
hence y in the carrier of G1 \/ the carrier of G2 by XBOOLE_0:def 3; :: thesis: S1[x,y]
thus S1[x,y] by A20; :: thesis: verum
end;
hence ex y being object st
( y in the carrier of G1 \/ the carrier of G2 & S1[x,y] ) by A17; :: 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 x being object st x in the carrier' of G1 \/ the carrier' of G2 holds
S1[x,S . x] from FUNCT_2:sch 1(A15);
 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 A23: 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 A22, A23; :: thesis: verum
end;
let v be set ; :: thesis: ( v in the carrier' of G2 implies S . v = the Target of G2 . v )
assume A24: 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 A22, A24; :: 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
A25: for v being set st v in the carrier' of G1 holds
T . v = the Target of G1 . v and
A26: 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 A13, A25; :: 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 A27: 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 A14; :: thesis: the Target of G . v = the Target of G2 . v
thus the Target of G . v = the Target of G2 . v by A26, A27; :: thesis: verum