let G1, G2 be EGraph; :: thesis: for H being ESubgraph of G2
for F being PGraphMapping of G1,G2 st F is elabel-preserving holds
H |` F is elabel-preserving
let H be ESubgraph of G2; :: thesis: for F being PGraphMapping of G1,G2 st F is elabel-preserving holds
H |` F is elabel-preserving
let F be PGraphMapping of G1,G2; :: thesis: ( F is elabel-preserving implies H |` F is elabel-preserving )
assume A1: F is elabel-preserving ; :: thesis: H |` F is elabel-preserving
(the_Edges_of H) |` (F _E) c= F _E by RELAT_1:86;
then A2: (dom ((the_Edges_of H) |` (F _E))) /\ (dom (F _E)) = dom ((H |` F) _E) by XBOOLE_1:28, RELAT_1:11;
(the_ELabel_of H) * ((H |` F) _E) = ((the_ELabel_of G2) | (the_Edges_of H)) * ((H |` F) _E) by GLIB_003:def 11
.= (the_ELabel_of G2) * ((the_Edges_of H) |` ((the_Edges_of H) |` (F _E))) by GROUP_9:121
.= (the_ELabel_of G2) * ((F _E) | (dom ((the_Edges_of H) |` (F _E)))) by GLIB_009:4
.= ((the_ELabel_of G1) | (dom (F _E))) | (dom ((H |` F) _E)) by A1, RELAT_1:83
.= (the_ELabel_of G1) | (dom ((H |` F) _E)) by A2, RELAT_1:71 ;
hence H |` F is elabel-preserving ; :: thesis: verum