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, Th16;
then A3: F ?- (dom f) is_transformable_to F ?- (dom g) by NATTRA_1:def 7;
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 Th16;
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 Th16;
then A7: F ?- (dom (g (*) f)) is_transformable_to F ?- (cod (g (*) f)) by NATTRA_1:def 7;

A8: now :: thesis: for b being Object of B holds (F ?- (g (*) f)) . b = ((F ?- g) `*` s) . b

let b be Object of B; :: thesis: (F ?- (g (*) f)) . b = ((F ?- g) `*` s) . b
A9: Hom (b,b) <> {} ;
A10: id b = (IdMap B) . b by ISOCAT_1:def 12;
A11: (F ?- g) . b = ((curry (F,g)) * (IdMap B)) . b by A6, NATTRA_1:def 5
.= Fg . (id b) by FUNCT_2:15, A10
.= F . (g,(id b)) by FUNCT_5:69 ;
dom (id b) = b
.= cod (id b) ;
then A12: dom [g,(id b)] = [(cod f),(cod (id b))] by A1, CAT_2:28
.= cod [f,(id b)] by CAT_2:28 ;
A13: ( 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;
A14: (F ?- f) . b = ((curry (F,f)) * (IdMap B)) . b by A1, A3, NATTRA_1:def 5
.= Ff . (id b) by FUNCT_2:15, A10
.= F . (f,(id b)) by FUNCT_5:69 ;
thus (F ?- (g (*) f)) . b = ((curry (F,(g (*) f))) * (IdMap B)) . b by A7, NATTRA_1:def 5
.= Fgf . (id b) by FUNCT_2:15, A10
.= F . ((g (*) f),(id b)) by FUNCT_5:69
.= F . [(g (*) f),((id b) * (id b))]
.= F . [(g (*) f),((id b) (*) (id b))] by A9, CAT_1:def 13
.= F . ([g,(id b)] (*) [f,(id b)]) by A12, CAT_2:30
.= ((F ?- g) . b) (*) (s . b) by A1, A4, A11, A14, A12, CAT_1:64
.= ((F ?- g) . b) * (s . b) by A13, 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: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