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

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

F | H is vlabel-preserving

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

F | H is vlabel-preserving

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

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

(the_VLabel_of G2) * ((F | H) _V) = ((the_VLabel_of G2) * (F _V)) | (the_Vertices_of H) by RELAT_1:83

.= (the_VLabel_of G1) | ((dom (F _V)) /\ ((the_Vertices_of H) /\ (the_Vertices_of H))) by A1, RELAT_1:71

.= (the_VLabel_of G1) | ((the_Vertices_of H) /\ ((dom (F _V)) /\ (the_Vertices_of H))) by XBOOLE_1:16

.= (the_VLabel_of G1) | ((the_Vertices_of H) /\ (dom ((F | H) _V))) by Th59

.= ((the_VLabel_of G1) | (the_Vertices_of H)) | (dom ((F | H) _V)) by RELAT_1:71

.= (the_VLabel_of H) | (dom ((F | H) _V)) by GLIB_003:def 12 ;

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

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

F | H is vlabel-preserving

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

F | H is vlabel-preserving

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

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

(the_VLabel_of G2) * ((F | H) _V) = ((the_VLabel_of G2) * (F _V)) | (the_Vertices_of H) by RELAT_1:83

.= (the_VLabel_of G1) | ((dom (F _V)) /\ ((the_Vertices_of H) /\ (the_Vertices_of H))) by A1, RELAT_1:71

.= (the_VLabel_of G1) | ((the_Vertices_of H) /\ ((dom (F _V)) /\ (the_Vertices_of H))) by XBOOLE_1:16

.= (the_VLabel_of G1) | ((the_Vertices_of H) /\ (dom ((F | H) _V))) by Th59

.= ((the_VLabel_of G1) | (the_Vertices_of H)) | (dom ((F | H) _V)) by RELAT_1:71

.= (the_VLabel_of H) | (dom ((F | H) _V)) by GLIB_003:def 12 ;

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