let o1, o2, o3 be Object of A; :: according to FUNCTOR0:def 23 :: 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) . b2) * ((G * F) . b1) )

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) . b2) * ((G * F) . b1)

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