let G1, G2, G3 be VGraph; :: thesis: for F1 being PGraphMapping of G1,G2

for F2 being PGraphMapping of G2,G3 st F1 is vlabel-preserving & F2 is vlabel-preserving holds

F2 * F1 is vlabel-preserving

let F1 be PGraphMapping of G1,G2; :: thesis: for F2 being PGraphMapping of G2,G3 st F1 is vlabel-preserving & F2 is vlabel-preserving holds

F2 * F1 is vlabel-preserving

let F2 be PGraphMapping of G2,G3; :: thesis: ( F1 is vlabel-preserving & F2 is vlabel-preserving implies F2 * F1 is vlabel-preserving )

assume A1: ( F1 is vlabel-preserving & F2 is vlabel-preserving ) ; :: thesis: F2 * F1 is vlabel-preserving

thus (the_VLabel_of G3) * ((F2 * F1) _V) = ((the_VLabel_of G3) * (F2 _V)) * (F1 _V) by RELAT_1:36

.= (the_VLabel_of G1) | (dom ((F2 * F1) _V)) by A1, Th1 ; :: according to GLIB_010:def 27 :: thesis: verum

for F2 being PGraphMapping of G2,G3 st F1 is vlabel-preserving & F2 is vlabel-preserving holds

F2 * F1 is vlabel-preserving

let F1 be PGraphMapping of G1,G2; :: thesis: for F2 being PGraphMapping of G2,G3 st F1 is vlabel-preserving & F2 is vlabel-preserving holds

F2 * F1 is vlabel-preserving

let F2 be PGraphMapping of G2,G3; :: thesis: ( F1 is vlabel-preserving & F2 is vlabel-preserving implies F2 * F1 is vlabel-preserving )

assume A1: ( F1 is vlabel-preserving & F2 is vlabel-preserving ) ; :: thesis: F2 * F1 is vlabel-preserving

thus (the_VLabel_of G3) * ((F2 * F1) _V) = ((the_VLabel_of G3) * (F2 _V)) * (F1 _V) by RELAT_1:36

.= (the_VLabel_of G1) | (dom ((F2 * F1) _V)) by A1, Th1 ; :: according to GLIB_010:def 27 :: thesis: verum