let G1, G2 be WGraph; :: thesis: for H being WSubgraph of G1
for F being PGraphMapping of G1,G2 st F is weight-preserving holds
F | H is weight-preserving
let H be WSubgraph of G1; :: thesis: for F being PGraphMapping of G1,G2 st F is weight-preserving holds
F | H is weight-preserving
let F be PGraphMapping of G1,G2; :: thesis: ( F is weight-preserving implies F | H is weight-preserving )
assume A1: F is weight-preserving ; :: thesis: F | H is weight-preserving
(the_Weight_of G2) * ((F | H) _E) = ((the_Weight_of G2) * (F _E)) | (the_Edges_of H) by RELAT_1:83
.= (the_Weight_of G1) | ((dom (F _E)) /\ ((the_Edges_of H) /\ (the_Edges_of H))) by A1, RELAT_1:71
.= (the_Weight_of G1) | ((the_Edges_of H) /\ ((dom (F _E)) /\ (the_Edges_of H))) by XBOOLE_1:16
.= (the_Weight_of G1) | ((the_Edges_of H) /\ (dom ((F | H) _E))) by Th59
.= ((the_Weight_of G1) | (the_Edges_of H)) | (dom ((F | H) _E)) by RELAT_1:71
.= (the_Weight_of H) | (dom ((F | H) _E)) by GLIB_003:def 10 ;
hence F | H is weight-preserving ; :: thesis: verum