let C1 be non empty AltGraph ; 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 ; 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; 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; for H being FunctorStr over C3,C4 holds (H * G) * F = H * (G * F)
let H be FunctorStr over C3,C4; (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; verum