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)) * the Id of 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)) * the Id of 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)) * the Id of 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)) * the Id of B is natural_transformation of F ?- a1,F ?- a2 )
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 ;
let f be Morphism of a1,a2; :: thesis: ( F ?- a1 is_naturally_transformable_to F ?- a2 & (curry (F,f)) * the Id of 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

let b be Object of B; :: thesis: ((curry (F,f)) * the Id of 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:26, CAT_1:def 4;
then [f,(id b)] in Hom ([a1,b],[a2,b]) by Th16;
then A3: F . (f,(id b)) in Hom ((F . [a1,b]),(F . [a2,b])) by CAT_1:81;
( (F ?- a1) . b = F . [a1,b] & (F ?- a2) . b = F . [a2,b] ) by Th12;
then Ff . (id b) in Hom (((F ?- a1) . b),((F ?- a2) . b)) by A3, CAT_2:3;
hence ((curry (F,f)) * the Id of B) . b in Hom (((F ?- a1) . b),((F ?- a2) . b)) by FUNCT_2:15; :: thesis: verum

end;

A4: F ?- a1 is_transformable_to F ?- a2

proof

let b be Object of B; :: according to NATTRA_1:def 2 :: thesis: not Hom (((F ?- a1) . b),((F ?- a2) . b)) = {}
thus not Hom (((F ?- a1) . b),((F ?- a2) . b)) = {} by A2; :: thesis: verum

end;

reconsider FfI = (curry (F,f)) * the Id of B as Function of the carrier of B, the carrier' of C ;

now

let b be Object of B; :: thesis: FfI . b is Morphism of (F ?- a1) . b,(F ?- a2) . b
((curry (F,f)) * the Id of 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 4; :: thesis: verum

end;

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

A5: now

reconsider ida1 = id a1, ida2 = id a2 as Morphism of A ;
A6: Hom (a1,a1) <> {} by CAT_1:27;
A7: Hom (a2,a2) <> {} by CAT_1:27;
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 A8: Hom (b1,b2) <> {} ; :: thesis: for g being Morphism of b1,b2 holds (t . b2) * ((F ?- a1) . g) = ((F ?- a2) . g) * (t . b1)
A9: Hom (((F ?- a2) . b1),((F ?- a2) . b2)) <> {} by A8, 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 ;
A10: Hom (b1,b1) <> {} by CAT_1:27;
A11: dom (id b2) = b2 by CAT_1:19
.= cod g by A8, CAT_1:5 ;
Hom (b2,b2) <> {} by CAT_1:27;
then A12: [(f * ida1),(idb2 * g)] = [(f * ida1),((id b2) * g)] by A8, CAT_1:def 10
.= [(f * ida1),g] by A8, CAT_1:28
.= [(f * (id a1)),g] by A1, A6, CAT_1:def 10
.= [f,g] by A1, CAT_1:29
.= [((id a2) * f),g] by A1, CAT_1:28
.= [(ida2 * f),g] by A1, A7, CAT_1:def 10
.= [(ida2 * f),(g * (id b1))] by A8, CAT_1:29
.= [(ida2 * f),(g * idb1)] by A8, A10, CAT_1:def 10 ;
A13: ( Hom (((F ?- a1) . b2),((F ?- a2) . b2)) <> {} & t . b2 = FfI . b2 ) by A4, NATTRA_1:def 2, NATTRA_1:def 5;
A14: cod (id a1) = a1 by CAT_1:19
.= dom f by A1, CAT_1:5 ;
then A15: cod [(id a1),g] = [(dom f),(cod g)] by CAT_2:28
.= dom [f,(id b2)] by A11, CAT_2:28 ;
A16: ( Hom (((F ?- a1) . b1),((F ?- a2) . b1)) <> {} & t . b1 = FfI . b1 ) by A4, NATTRA_1:def 2, NATTRA_1:def 5;
A17: dom g = b1 by A8, CAT_1:5
.= cod (id b1) by CAT_1:19 ;
A18: dom (id a2) = a2 by CAT_1:19
.= cod f by A1, CAT_1:5 ;
then A19: dom [(id a2),g] = [(cod f),(dom g)] by CAT_2:28
.= cod [f,(id b1)] by A17, CAT_2:28 ;
Hom (((F ?- a1) . b1),((F ?- a1) . b2)) <> {} by A8, CAT_1:84;
hence (t . b2) * ((F ?- a1) . g) = (FfI . b2) * ((F ?- a1) . g) by A13, CAT_1:def 10
.= (Ff . (id b2)) * ((F ?- a1) . g) by FUNCT_2:15
.= (F . (f,(id b2))) * ((F ?- a1) . g) by CAT_2:3
.= (F . [f,(id b2)]) * ((F ?- a1) . g) by A8, NATTRA_1:def 1
.= (F . (f,(id b2))) * (F . ((id a1),g)) by CAT_2:36
.= F . ([f,(id b2)] * [(id a1),g]) by A15, CAT_1:64
.= F . [(f * ida1),(idb2 * g)] by A14, A11, CAT_2:29
.= F . ([ida2,g] * [f,idb1]) by A18, A17, A12, CAT_2:29
.= (F . ((id a2),g)) * (F . [f,(id b1)]) by A19, CAT_1:64
.= ((F ?- a2) . g) * (F . [f,(id b1)]) by CAT_2:36
.= ((F ?- a2) . g) * (F . (f,(id b1))) by A8, NATTRA_1:def 1
.= ((F ?- a2) . g) * (Ff . (id b1)) by CAT_2:3
.= ((F ?- a2) . g) * (FfI . b1) by FUNCT_2:15
.= ((F ?- a2) . g) * (t . b1) by A9, A16, CAT_1:def 10 ;
:: thesis: verum

end;

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