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

for F2 being PGraphMapping of G2,G3

for F3 being PGraphMapping of G3,G4 holds F3 * (F2 * F1) = (F3 * F2) * F1

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

for F3 being PGraphMapping of G3,G4 holds F3 * (F2 * F1) = (F3 * F2) * F1

let F2 be PGraphMapping of G2,G3; :: thesis: for F3 being PGraphMapping of G3,G4 holds F3 * (F2 * F1) = (F3 * F2) * F1

let F3 be PGraphMapping of G3,G4; :: thesis: F3 * (F2 * F1) = (F3 * F2) * F1

thus F3 * (F2 * F1) = [(((F3 _V) * (F2 _V)) * (F1 _V)),((F3 _E) * ((F2 _E) * (F1 _E)))] by RELAT_1:36

.= (F3 * F2) * F1 by RELAT_1:36 ; :: thesis: verum

for F2 being PGraphMapping of G2,G3

for F3 being PGraphMapping of G3,G4 holds F3 * (F2 * F1) = (F3 * F2) * F1

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

for F3 being PGraphMapping of G3,G4 holds F3 * (F2 * F1) = (F3 * F2) * F1

let F2 be PGraphMapping of G2,G3; :: thesis: for F3 being PGraphMapping of G3,G4 holds F3 * (F2 * F1) = (F3 * F2) * F1

let F3 be PGraphMapping of G3,G4; :: thesis: F3 * (F2 * F1) = (F3 * F2) * F1

thus F3 * (F2 * F1) = [(((F3 _V) * (F2 _V)) * (F1 _V)),((F3 _E) * ((F2 _E) * (F1 _E)))] by RELAT_1:36

.= (F3 * F2) * F1 by RELAT_1:36 ; :: thesis: verum