let G1 be _Graph; :: thesis: for G2 being Subgraph of G1 holds
( the_Source_of G2 = (the_Source_of G1) | (the_Edges_of G2) & the_Target_of G2 = (the_Target_of G1) | (the_Edges_of G2) )
let G2 be Subgraph of G1; :: thesis: ( the_Source_of G2 = (the_Source_of G1) | (the_Edges_of G2) & the_Target_of G2 = (the_Target_of G1) | (the_Edges_of G2) )
set S2 = (the_Source_of G1) | (the_Edges_of G2);
set T2 = (the_Target_of G1) | (the_Edges_of G2);

A1: now :: thesis: for x being object st x in dom (the_Source_of G2) holds
(the_Source_of G2) . x = ((the_Source_of G1) | (the_Edges_of G2)) . x

let x be object ; :: thesis: ( x in dom (the_Source_of G2) implies (the_Source_of G2) . x = ((the_Source_of G1) | (the_Edges_of G2)) . x )
assume A2: x in dom (the_Source_of G2) ; :: thesis: (the_Source_of G2) . x = ((the_Source_of G1) | (the_Edges_of G2)) . x
hence (the_Source_of G2) . x = (the_Source_of G1) . x by Def32
.= ((the_Source_of G1) | (the_Edges_of G2)) . x by A2, FUNCT_1:49 ;
:: thesis: verum

end;

dom (the_Source_of G1) = the_Edges_of G1 by FUNCT_2:def 1;
then ( dom (the_Source_of G2) = the_Edges_of G2 & dom ((the_Source_of G1) | (the_Edges_of G2)) = the_Edges_of G2 ) by FUNCT_2:def 1, RELAT_1:62;
hence the_Source_of G2 = (the_Source_of G1) | (the_Edges_of G2) by A1, FUNCT_1:2; :: thesis: the_Target_of G2 = (the_Target_of G1) | (the_Edges_of G2)

A3: now :: thesis: for x being object st x in dom (the_Target_of G2) holds
(the_Target_of G2) . x = ((the_Target_of G1) | (the_Edges_of G2)) . x

let x be object ; :: thesis: ( x in dom (the_Target_of G2) implies (the_Target_of G2) . x = ((the_Target_of G1) | (the_Edges_of G2)) . x )
assume A4: x in dom (the_Target_of G2) ; :: thesis: (the_Target_of G2) . x = ((the_Target_of G1) | (the_Edges_of G2)) . x
hence (the_Target_of G2) . x = (the_Target_of G1) . x by Def32
.= ((the_Target_of G1) | (the_Edges_of G2)) . x by A4, FUNCT_1:49 ;
:: thesis: verum

end;

dom (the_Target_of G1) = the_Edges_of G1 by FUNCT_2:def 1;
then ( dom (the_Target_of G2) = the_Edges_of G2 & dom ((the_Target_of G1) | (the_Edges_of G2)) = the_Edges_of G2 ) by FUNCT_2:def 1, RELAT_1:62;
hence the_Target_of G2 = (the_Target_of G1) | (the_Edges_of G2) by A3, FUNCT_1:2; :: thesis: verum