let o1, o2, o3 be Object of A; FUNCTOR0:def 24 ( <^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^> <> {}
; 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 . o1),(F . o2)^> <> {} & <^(F . o2),(F . o3)^> <> {} )
by A1, A2, FUNCTOR0:def 18;
let f be Morphism of o1,o2; for b1 being M3(<^o2,o3^>) holds (G * F) . (b1 * f) = ((G * F) . f) * ((G * F) . b1)
let g be Morphism of o2,o3; (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 A1, A2, ALTCAT_1:def 2;
hence (G * F) . (g * f) =
G . (F . (g * f))
by Th8
.=
G . ((F . g) * (F . f))
by A1, A2, FUNCTOR0:def 23
.=
(G . (F . f)) * (G . (F . g))
by A3, FUNCTOR0:def 24
.=
GFf * (G . (F . g))
by A1, Th8
.=
((G * F) . f) * ((G * F) . g)
by A2, A5, A4, Th8
;
verum