let C1 be non empty AltCatStr ; :: thesis: for C2, C3 being non empty reflexive AltCatStr
for F being reflexive feasible FunctorStr over C1,C2
for G being FunctorStr over C2,C3
for o being Object of C1 holds (G * F) . o = G . (F . o)
let C2, C3 be non empty reflexive AltCatStr ; :: thesis: for F being reflexive feasible FunctorStr over C1,C2
for G being FunctorStr over C2,C3
for o being Object of C1 holds (G * F) . o = G . (F . o)
let F be reflexive feasible FunctorStr over C1,C2; :: thesis: for G being FunctorStr over C2,C3
for o being Object of C1 holds (G * F) . o = G . (F . o)
let G be FunctorStr over C2,C3; :: thesis: for o being Object of C1 holds (G * F) . o = G . (F . o)
let o be Object of C1; :: thesis: (G * F) . o = G . (F . o)
dom the ObjectMap of F = [: the carrier of C1, the carrier of C1:] by FUNCT_2:def 1;
then A1: [o,o] in dom the ObjectMap of F by ZFMISC_1:87;
thus (G * F) . o = (( the ObjectMap of G * the ObjectMap of F) . (o,o)) `1 by Def36
.= ( the ObjectMap of G . ( the ObjectMap of F . [o,o])) `1 by A1, FUNCT_1:13
.= G . (F . o) by Def10 ; :: thesis: verum