let o1, o2, o3 be Object of A; :: according to FUNCTOR0:def 24 :: thesis: ( <^o1,o2^> = {} or <^o2,o3^> = {} or for b1 being M3(<^o1,o2^>)
for b2 being M3(<^o2,o3^>) holds (G * F) . (b2 * b1) = ((G * F) . b1) * ((G * F) . b2) )

assume that
A1: <^o1,o2^> <> {} and
A2: <^o2,o3^> <> {} ; :: thesis: for b1 being M3(<^o1,o2^>)
for b2 being M3(<^o2,o3^>) holds (G * F) . (b2 * b1) = ((G * F) . b1) * ((G * F) . b2)

A3: ( <^(F . o2),(F . o1)^> <> {} & <^(F . o3),(F . o2)^> <> {} ) by ;
let f be Morphism of o1,o2; :: thesis: for b1 being M3(<^o2,o3^>) holds (G * F) . (b1 * f) = ((G * F) . f) * ((G * F) . b1)
let g be Morphism of o2,o3; :: thesis: (G * F) . (g * f) = ((G * F) . f) * ((G * F) . g)
A4: ( (G * F) . o2 = G . (F . o2) & (G * F) . o3 = G . (F . o3) ) by FUNCTOR0:33;
A5: (G * F) . o1 = G . (F . o1) by FUNCTOR0:33;
then reconsider GFf = (G * F) . f as Morphism of (G . (F . o2)),(G . (F . o1)) by FUNCTOR0:33;
<^o1,o3^> <> {} by ;
hence (G * F) . (g * f) = G . (F . (g * f)) by Th9
.= G . ((F . f) * (F . g)) by
.= (G . (F . f)) * (G . (F . g)) by
.= GFf * (G . (F . g)) by
.= ((G * F) . f) * ((G * F) . g) by A2, A5, A4, Th9 ;
:: thesis: verum