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:23;
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:27;
A10: (F ?- g) . b = ((curry (F,g)) * the Id of B) . b by A6, NATTRA_1:def 5
.= Fg . (id b) by FUNCT_2:15
.= F . (g,(id b)) by CAT_2:3 ;
dom (id b) = b by CAT_1:19
.= cod (id b) by CAT_1:19 ;
then A11: dom [g,(id b)] = [(cod f),(cod (id b))] by A1, CAT_2:28
.= cod [f,(id b)] by CAT_2:28 ;
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:15
.= 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:15
.= F . ((g * f),(id b)) by CAT_2:3
.= F . [(g * f),((id b) * (id b))] by CAT_1:30
.= F . [(g * f),((id b) * (id b))] by A9, CAT_1:def 10
.= F . ([g,(id b)] * [f,(id b)]) by A11, CAT_2:30
.= ((F ?- g) . b) * (s . b) by A1, A4, A10, A13, A11, CAT_1:64
.= ((F ?- g) . b) * (s . b) by A12, CAT_1:def 10
.= ((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:17;
then F ?- (g * f) = (F ?- g) `*` s by A3, A6, A8, NATTRA_1:18, NATTRA_1:19;
hence F ?- (g * f) = (F ?- g) `*` t by A2, A5, NATTRA_1:def 9; :: thesis: verum