let C1 be non empty AltCatStr ; :: thesis: for C2, C3 being non empty reflexive AltCatStr
for F being reflexive feasible FunctorStr of C1,C2
for G being FunctorStr of 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 of C1,C2
for G being FunctorStr of C2,C3
for o being object of C1 holds (G * F) . o = G . (F . o)
let F be reflexive feasible FunctorStr of C1,C2; :: thesis: for G being FunctorStr of C2,C3
for o being object of C1 holds (G * F) . o = G . (F . o)
let G be FunctorStr of 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:106;
thus (G * F) . o = ((the ObjectMap of G * the ObjectMap of F) . o,o) `1 by Def37
.= (the ObjectMap of G . (the ObjectMap of F . [o,o])) `1 by A1, FUNCT_1:23
.= G . (F . o) by Def11 ; :: thesis: verum