let A, B, C be Category; :: thesis: for F being Functor of [:A,B:],C
for g, f being Morphism of A st dom g = cod f holds
for t being natural_transformation of F ?- (dom f),F ?- (dom g) st t = F ?- f holds
F ?- (g * f) = (F ?- g) `*` t
let F be Functor of [:A,B:],C; :: thesis: for g, f being Morphism of A st dom g = cod f holds
for t being natural_transformation of F ?- (dom f),F ?- (dom g) st t = F ?- f holds
F ?- (g * f) = (F ?- g) `*` t
let g, f be Morphism of A; :: thesis: ( dom g = cod f implies for t being natural_transformation of F ?- (dom f),F ?- (dom g) st t = F ?- f holds
F ?- (g * f) = (F ?- g) `*` t )
assume A1: dom g = cod f ; :: thesis: for t being natural_transformation of F ?- (dom f),F ?- (dom g) st t = F ?- f holds
F ?- (g * f) = (F ?- g) `*` t
A2: F ?- (dom f) is_naturally_transformable_to F ?- (dom g) by A1, Th18;
then A3: F ?- (dom f) is_transformable_to F ?- (dom g) by NATTRA_1:def 7;
the carrier' of [:A,B:] = [:the carrier' of A,the carrier' of B:] by CAT_2:33;
then reconsider G = F as Function of [:the carrier' of A,the carrier' of B:],the carrier' of C ;
reconsider Fgf = (curry G) . (g * f), Ff = (curry G) . f, Fg = (curry G) . g as Function of the carrier' of B,the carrier' of C ;
let t be natural_transformation of F ?- (dom f),F ?- (dom g); :: thesis: ( t = F ?- f implies F ?- (g * f) = (F ?- g) `*` t )
assume A4: t = F ?- f ; :: thesis: F ?- (g * f) = (F ?- g) `*` t
reconsider s = t as transformation of F ?- (dom f),F ?- (dom g) ;
A5: F ?- (dom g) is_naturally_transformable_to F ?- (cod g) by Th18;
then A6: F ?- (dom g) is_transformable_to F ?- (cod g) by NATTRA_1:def 7;
F ?- (dom (g * f)) is_naturally_transformable_to F ?- (cod (g * f)) by Th18;
then A7: F ?- (dom (g * f)) is_transformable_to F ?- (cod (g * f)) by NATTRA_1:def 7;

A8: now

let b be Object of B; :: thesis: (F ?- (g * f)) . b = ((F ?- g) `*` s) . b
A9: Hom b,b <> {} by CAT_1:56;
A10: (F ?- g) . b = ((curry F,g) * the Id of B) . b by A6, NATTRA_1:def 5
.= Fg . (id b) by FUNCT_2:21
.= F . g,(id b) by CAT_2:3 ;
dom (id b) = b by CAT_1:44
.= cod (id b) by CAT_1:44 ;
then A11: dom [g,(id b)] = [(cod f),(cod (id b))] by A1, CAT_2:38
.= cod [f,(id b)] by CAT_2:38 ;
A12: ( Hom ((F ?- (dom g)) . b),((F ?- (cod g)) . b) <> {} & Hom ((F ?- (dom f)) . b),((F ?- (dom g)) . b) <> {} ) by A3, A6, NATTRA_1:def 2;
A13: (F ?- f) . b = ((curry F,f) * the Id of B) . b by A1, A3, NATTRA_1:def 5
.= Ff . (id b) by FUNCT_2:21
.= F . f,(id b) by CAT_2:3 ;
thus (F ?- (g * f)) . b = ((curry F,(g * f)) * the Id of B) . b by A7, NATTRA_1:def 5
.= Fgf . (id b) by FUNCT_2:21
.= F . (g * f),(id b) by CAT_2:3
.= F . [(g * f),((id b) * (id b))] by CAT_1:59
.= F . [(g * f),((id b) * (id b))] by A9, CAT_1:def 13
.= F . ([g,(id b)] * [f,(id b)]) by A11, CAT_2:40
.= ((F ?- g) . b) * (s . b) by A1, A4, A10, A13, A11, CAT_1:99
.= ((F ?- g) . b) * (s . b) by A12, CAT_1:def 13
.= ((F ?- g) `*` s) . b by A3, A6, NATTRA_1:def 6 ; :: thesis: verum

end;

( cod (g * f) = cod g & dom (g * f) = dom f ) by A1, CAT_1:42;
then F ?- (g * f) = (F ?- g) `*` s by A3, A6, A8, NATTRA_1:19, NATTRA_1:20;
hence F ?- (g * f) = (F ?- g) `*` t by A2, A5, NATTRA_1:def 9; :: thesis: verum