let A, B, C be Category; :: thesis: for F being Functor of [:A,B:],C
for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds
( F ?- a is_naturally_transformable_to F ?- b & (curry (F,f)) * (IdMap B) is natural_transformation of F ?- a,F ?- b )
let F be Functor of [:A,B:],C; :: thesis: for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds
( F ?- a is_naturally_transformable_to F ?- b & (curry (F,f)) * (IdMap B) is natural_transformation of F ?- a,F ?- b )
let a1, a2 be Object of A; :: thesis: ( Hom (a1,a2) <> {} implies for f being Morphism of a1,a2 holds
( F ?- a1 is_naturally_transformable_to F ?- a2 & (curry (F,f)) * (IdMap B) is natural_transformation of F ?- a1,F ?- a2 ) )
assume A1: Hom (a1,a2) <> {} ; :: thesis: for f being Morphism of a1,a2 holds
( F ?- a1 is_naturally_transformable_to F ?- a2 & (curry (F,f)) * (IdMap B) is natural_transformation of F ?- a1,F ?- a2 )
reconsider G = F as Function of [: the carrier' of A, the carrier' of B:], the carrier' of C ;
let f be Morphism of a1,a2; :: thesis: ( F ?- a1 is_naturally_transformable_to F ?- a2 & (curry (F,f)) * (IdMap B) is natural_transformation of F ?- a1,F ?- a2 )
reconsider Ff = (curry G) . f as Function of the carrier' of B, the carrier' of C ;

A2: now :: thesis: for b being Object of B holds ((curry (F,f)) * (IdMap B)) . b in Hom (((F ?- a1) . b),((F ?- a2) . b))

let b be Object of B; :: thesis: ((curry (F,f)) * (IdMap B)) . b in Hom (((F ?- a1) . b),((F ?- a2) . b))
( f in Hom (a1,a2) & id b in Hom (b,b) ) by A1, CAT_1:def 5;
then [f,(id b)] in Hom ([a1,b],[a2,b]) by Th12;
then A3: F . (f,(id b)) in Hom ((F . [a1,b]),(F . [a2,b])) by CAT_1:81;
A4: id b = (IdMap B) . b by ISOCAT_1:def 12;
( (F ?- a1) . b = F . [a1,b] & (F ?- a2) . b = F . [a2,b] ) by Th8;
then Ff . (id b) in Hom (((F ?- a1) . b),((F ?- a2) . b)) by A3, FUNCT_5:69;
hence ((curry (F,f)) * (IdMap B)) . b in Hom (((F ?- a1) . b),((F ?- a2) . b)) by A4, FUNCT_2:15; :: thesis: verum

end;

A5: F ?- a1 is_transformable_to F ?- a2 by A2;
reconsider FfI = (curry (F,f)) * (IdMap B) as Function of the carrier of B, the carrier' of C ;

now :: thesis: for b being Object of B holds FfI . b is Morphism of (F ?- a1) . b,(F ?- a2) . b

let b be Object of B; :: thesis: FfI . b is Morphism of (F ?- a1) . b,(F ?- a2) . b
((curry (F,f)) * (IdMap B)) . b in Hom (((F ?- a1) . b),((F ?- a2) . b)) by A2;
hence FfI . b is Morphism of (F ?- a1) . b,(F ?- a2) . b by CAT_1:def 5; :: thesis: verum

end;

then reconsider t = (curry (F,f)) * (IdMap B) as transformation of F ?- a1,F ?- a2 by A5, NATTRA_1:def 3;

A6: now :: thesis: for b1, b2 being Object of B st Hom (b1,b2) <> {} holds
for g being Morphism of b1,b2 holds (t . b2) * ((F ?- a1) /. g) = ((F ?- a2) /. g) * (t . b1)

reconsider ida1 = id a1, ida2 = id a2 as Morphism of A ;
A7: Hom (a1,a1) <> {} ;
A8: Hom (a2,a2) <> {} ;
let b1, b2 be Object of B; :: thesis: ( Hom (b1,b2) <> {} implies for g being Morphism of b1,b2 holds (t . b2) * ((F ?- a1) /. g) = ((F ?- a2) /. g) * (t . b1) )
assume A9: Hom (b1,b2) <> {} ; :: thesis: for g being Morphism of b1,b2 holds (t . b2) * ((F ?- a1) /. g) = ((F ?- a2) /. g) * (t . b1)
A10: Hom (((F ?- a2) . b1),((F ?- a2) . b2)) <> {} by A9, CAT_1:84;
let g be Morphism of b1,b2; :: thesis: (t . b2) * ((F ?- a1) /. g) = ((F ?- a2) /. g) * (t . b1)
reconsider idb1 = id b1, idb2 = id b2 as Morphism of B ;
A11: Hom (b1,b1) <> {} ;
A12: dom (id b2) = b2
.= cod g by A9, CAT_1:5 ;
Hom (b2,b2) <> {} ;
then A13: [(f (*) ida1),(idb2 (*) g)] = [(f (*) ida1),((id b2) * g)] by A9, CAT_1:def 13
.= [(f (*) ida1),g] by A9, CAT_1:28
.= [(f * (id a1)),g] by A1, A7, CAT_1:def 13
.= [f,g] by A1, CAT_1:29
.= [((id a2) * f),g] by A1, CAT_1:28
.= [(ida2 (*) f),g] by A1, A8, CAT_1:def 13
.= [(ida2 (*) f),(g * (id b1))] by A9, CAT_1:29
.= [(ida2 (*) f),(g (*) idb1)] by A9, A11, CAT_1:def 13 ;
A14: ( Hom (((F ?- a1) . b2),((F ?- a2) . b2)) <> {} & t . b2 = FfI . b2 ) by A5, NATTRA_1:def 5;
A15: cod (id a1) = a1
.= dom f by A1, CAT_1:5 ;
then A16: cod [(id a1),g] = [(dom f),(cod g)] by CAT_2:28
.= dom [f,(id b2)] by A12, CAT_2:28 ;
A17: ( Hom (((F ?- a1) . b1),((F ?- a2) . b1)) <> {} & t . b1 = FfI . b1 ) by A5, NATTRA_1:def 5;
A18: dom g = b1 by A9, CAT_1:5
.= cod (id b1) ;
A19: dom (id a2) = a2
.= cod f by A1, CAT_1:5 ;
then A20: dom [(id a2),g] = [(cod f),(dom g)] by CAT_2:28
.= cod [f,(id b1)] by A18, CAT_2:28 ;
A21: id b2 = (IdMap B) . b2 by ISOCAT_1:def 12;
A22: id b1 = (IdMap B) . b1 by ISOCAT_1:def 12;
Hom (((F ?- a1) . b1),((F ?- a1) . b2)) <> {} by A9, CAT_1:84;
hence (t . b2) * ((F ?- a1) /. g) = (FfI . b2) (*) ((F ?- a1) /. g) by A14, CAT_1:def 13
.= (Ff . (id b2)) (*) ((F ?- a1) /. g) by A21, FUNCT_2:15
.= (F . (f,(id b2))) (*) ((F ?- a1) /. g) by FUNCT_5:69
.= (F . [f,(id b2)]) (*) ((F ?- a1) . g) by A9, CAT_3:def 10
.= (F . (f,(id b2))) (*) (F . ((id a1),g)) by CAT_2:36
.= F . ([f,(id b2)] (*) [(id a1),g]) by A16, CAT_1:64
.= F . [(f (*) ida1),(idb2 (*) g)] by A15, A12, CAT_2:29
.= F . ([ida2,g] (*) [f,idb1]) by A19, A18, A13, CAT_2:29
.= (F . ((id a2),g)) (*) (F . [f,(id b1)]) by A20, CAT_1:64
.= ((F ?- a2) . g) (*) (F . [f,(id b1)]) by CAT_2:36
.= ((F ?- a2) /. g) (*) (F . (f,(id b1))) by A9, CAT_3:def 10
.= ((F ?- a2) /. g) (*) (Ff . (id b1)) by FUNCT_5:69
.= ((F ?- a2) /. g) (*) (FfI . b1) by A22, FUNCT_2:15
.= ((F ?- a2) /. g) * (t . b1) by A10, A17, CAT_1:def 13 ;
:: thesis: verum

end;

hence F ?- a1 is_naturally_transformable_to F ?- a2 by A5; :: thesis: (curry (F,f)) * (IdMap B) is natural_transformation of F ?- a1,F ?- a2
hence (curry (F,f)) * (IdMap B) is natural_transformation of F ?- a1,F ?- a2 by A6, NATTRA_1:def 8; :: thesis: verum