let C1 be non empty AltGraph ; :: thesis: for C2, C3, C4 being non empty reflexive AltGraph
for F being feasible FunctorStr over C1,C2
for G being feasible FunctorStr over C2,C3
for H being FunctorStr over C3,C4 holds (H * G) * F = H * (G * F)
let C2, C3, C4 be non empty reflexive AltGraph ; :: thesis: for F being feasible FunctorStr over C1,C2
for G being feasible FunctorStr over C2,C3
for H being FunctorStr over C3,C4 holds (H * G) * F = H * (G * F)
let F be feasible FunctorStr over C1,C2; :: thesis: for G being feasible FunctorStr over C2,C3
for H being FunctorStr over C3,C4 holds (H * G) * F = H * (G * F)
let G be feasible FunctorStr over C2,C3; :: thesis: for H being FunctorStr over C3,C4 holds (H * G) * F = H * (G * F)
let H be FunctorStr over 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 Def36
.= ( the ObjectMap of H * the ObjectMap of G) * the ObjectMap of F by Def36
.= 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 Def36
.= the ObjectMap of (H * (G * F)) by Def36 ;
the MorphMap of ((H * G) * F) = ( the MorphMap of (H * G) * the ObjectMap of F) ** the MorphMap of F by Def36
.= ((( the MorphMap of H * the ObjectMap of G) ** the MorphMap of G) * the ObjectMap of F) ** the MorphMap of F by Def36
.= ((( 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 Th12
.= (( 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 Def36
.= ( 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 Def36
.= the MorphMap of (H * (G * F)) by Def36 ;
hence (H * G) * F = H * (G * F) by A1; :: thesis: verum