let G1, G2 be VGraph; :: thesis: for H being VSubgraph of G2

for F being PGraphMapping of G1,G2 st F is vlabel-preserving holds

H |` F is vlabel-preserving

let H be VSubgraph of G2; :: thesis: for F being PGraphMapping of G1,G2 st F is vlabel-preserving holds

H |` F is vlabel-preserving

let F be PGraphMapping of G1,G2; :: thesis: ( F is vlabel-preserving implies H |` F is vlabel-preserving )

assume A1: F is vlabel-preserving ; :: thesis: H |` F is vlabel-preserving

(the_Vertices_of H) |` (F _V) c= F _V by RELAT_1:86;

then A2: (dom ((the_Vertices_of H) |` (F _V))) /\ (dom (F _V)) = dom ((H |` F) _V) by XBOOLE_1:28, RELAT_1:11;

(the_VLabel_of H) * ((H |` F) _V) = ((the_VLabel_of G2) | (the_Vertices_of H)) * ((H |` F) _V) by GLIB_003:def 12

.= (the_VLabel_of G2) * ((the_Vertices_of H) |` ((the_Vertices_of H) |` (F _V))) by GROUP_9:121

.= (the_VLabel_of G2) * ((F _V) | (dom ((the_Vertices_of H) |` (F _V)))) by GLIB_009:4

.= ((the_VLabel_of G1) | (dom (F _V))) | (dom ((H |` F) _V)) by A1, RELAT_1:83

.= (the_VLabel_of G1) | (dom ((H |` F) _V)) by A2, RELAT_1:71 ;

hence H |` F is vlabel-preserving ; :: thesis: verum

for F being PGraphMapping of G1,G2 st F is vlabel-preserving holds

H |` F is vlabel-preserving

let H be VSubgraph of G2; :: thesis: for F being PGraphMapping of G1,G2 st F is vlabel-preserving holds

H |` F is vlabel-preserving

let F be PGraphMapping of G1,G2; :: thesis: ( F is vlabel-preserving implies H |` F is vlabel-preserving )

assume A1: F is vlabel-preserving ; :: thesis: H |` F is vlabel-preserving

(the_Vertices_of H) |` (F _V) c= F _V by RELAT_1:86;

then A2: (dom ((the_Vertices_of H) |` (F _V))) /\ (dom (F _V)) = dom ((H |` F) _V) by XBOOLE_1:28, RELAT_1:11;

(the_VLabel_of H) * ((H |` F) _V) = ((the_VLabel_of G2) | (the_Vertices_of H)) * ((H |` F) _V) by GLIB_003:def 12

.= (the_VLabel_of G2) * ((the_Vertices_of H) |` ((the_Vertices_of H) |` (F _V))) by GROUP_9:121

.= (the_VLabel_of G2) * ((F _V) | (dom ((the_Vertices_of H) |` (F _V)))) by GLIB_009:4

.= ((the_VLabel_of G1) | (dom (F _V))) | (dom ((H |` F) _V)) by A1, RELAT_1:83

.= (the_VLabel_of G1) | (dom ((H |` F) _V)) by A2, RELAT_1:71 ;

hence H |` F is vlabel-preserving ; :: thesis: verum