let C1 be non empty AltGraph ; :: thesis: for C2, C3, C4 being non empty reflexive AltGraph
for F being feasible FunctorStr of C1,C2
for G being feasible FunctorStr of C2,C3
for H being FunctorStr of C3,C4 holds (H * G) * F = H * (G * F)
let C2, C3, C4 be non empty reflexive AltGraph ; :: thesis: for F being feasible FunctorStr of C1,C2
for G being feasible FunctorStr of C2,C3
for H being FunctorStr of C3,C4 holds (H * G) * F = H * (G * F)
let F be feasible FunctorStr of C1,C2; :: thesis: for G being feasible FunctorStr of C2,C3
for H being FunctorStr of C3,C4 holds (H * G) * F = H * (G * F)
let G be feasible FunctorStr of C2,C3; :: thesis: for H being FunctorStr of C3,C4 holds (H * G) * F = H * (G * F)
let H be FunctorStr of C3,C4; :: thesis: (H * G) * F = H * (G * F)
A1: the ObjectMap of ((H * G) * F) = the ObjectMap of (H * G) * the ObjectMap of F by Def37
.= ( the ObjectMap of H * the ObjectMap of G) * the ObjectMap of F by Def37
.= the ObjectMap of H * ( the ObjectMap of G * the ObjectMap of F) by RELAT_1:36
.= the ObjectMap of H * the ObjectMap of (G * F) by Def37
.= the ObjectMap of (H * (G * F)) by Def37 ;
the MorphMap of ((H * G) * F) = ( the MorphMap of (H * G) * the ObjectMap of F) ** the MorphMap of F by Def37
.= ((( the MorphMap of H * the ObjectMap of G) ** the MorphMap of G) * the ObjectMap of F) ** the MorphMap of F by Def37
.= ((( the MorphMap of H * the ObjectMap of G) * the ObjectMap of F) ** ( the MorphMap of G * the ObjectMap of F)) ** the MorphMap of F by Th13
.= (( the MorphMap of H * ( the ObjectMap of G * the ObjectMap of F)) ** ( the MorphMap of G * the ObjectMap of F)) ** the MorphMap of F by RELAT_1:36
.= (( the MorphMap of H * the ObjectMap of (G * F)) ** ( the MorphMap of G * the ObjectMap of F)) ** the MorphMap of F by Def37
.= ( the MorphMap of H * the ObjectMap of (G * F)) ** (( the MorphMap of G * the ObjectMap of F) ** the MorphMap of F) by PBOOLE:140
.= ( the MorphMap of H * the ObjectMap of (G * F)) ** the MorphMap of (G * F) by Def37
.= the MorphMap of (H * (G * F)) by Def37 ;
hence (H * G) * F = H * (G * F) by A1; :: thesis: verum