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

for F2 being PGraphMapping of G2,G3 st F2 * F1 is total holds

F1 is total

let F1 be PGraphMapping of G1,G2; :: thesis: for F2 being PGraphMapping of G2,G3 st F2 * F1 is total holds

F1 is total

let F2 be PGraphMapping of G2,G3; :: thesis: ( F2 * F1 is total implies F1 is total )

assume F2 * F1 is total ; :: thesis: F1 is total

then ( the_Vertices_of G1 c= dom (F1 _V) & the_Edges_of G1 c= dom (F1 _E) ) by RELAT_1:25;

hence F1 is total by XBOOLE_0:def 10; :: thesis: verum

for F2 being PGraphMapping of G2,G3 st F2 * F1 is total holds

F1 is total

let F1 be PGraphMapping of G1,G2; :: thesis: for F2 being PGraphMapping of G2,G3 st F2 * F1 is total holds

F1 is total

let F2 be PGraphMapping of G2,G3; :: thesis: ( F2 * F1 is total implies F1 is total )

assume F2 * F1 is total ; :: thesis: F1 is total

then ( the_Vertices_of G1 c= dom (F1 _V) & the_Edges_of G1 c= dom (F1 _E) ) by RELAT_1:25;

hence F1 is total by XBOOLE_0:def 10; :: thesis: verum