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: ( dom (the_Source_of G1) = the_Edges_of G1 & dom (the_Target_of G1) = the_Edges_of G1 & dom (the_Source_of G2) = the_Edges_of G2 & dom (the_Target_of G2) = the_Edges_of G2 ) by FUNCT_2:def 1;
then A2: ( dom ((the_Source_of G1) | (the_Edges_of G2)) = the_Edges_of G2 & dom ((the_Target_of G1) | (the_Edges_of G2)) = the_Edges_of G2 ) by RELAT_1:91;

now

let x be set ; :: thesis: ( x in dom (the_Source_of G2) implies (the_Source_of G2) . x = ((the_Source_of G1) | (the_Edges_of G2)) . x )
assume A3: 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 Def34
.= ((the_Source_of G1) | (the_Edges_of G2)) . x by A3, FUNCT_1:72 ;
:: thesis: verum

end;

hence the_Source_of G2 = (the_Source_of G1) | (the_Edges_of G2) by A1, A2, FUNCT_1:9; :: thesis: the_Target_of G2 = (the_Target_of G1) | (the_Edges_of G2)

now

let x be set ; :: 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 Def34
.= ((the_Target_of G1) | (the_Edges_of G2)) . x by A4, FUNCT_1:72 ;
:: thesis: verum

end;

hence the_Target_of G2 = (the_Target_of G1) | (the_Edges_of G2) by A1, A2, FUNCT_1:9; :: thesis: verum