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