let C1, C2 be non empty category; :: thesis:
let F1, F2 be covariant Functor of C1,C2; :: thesis:
let T be Function of (Ob C1),(Mor C2); :: thesis:

hereby :: thesis:

given T1 being Functor of C1,C2 such that A1: T = T1 | (Ob C1) and
A2: T1 is_natural_transformation_of F1,F2 ; :: thesis:
thus for a being Object of C1 holds T . a in Hom ((F1 . a),(F2 . a)) :: thesis:

proof

let a be Object of C1; :: thesis:
a in Ob C1 ;
then a in { f where f is morphism of C1 : ( f is identity & f in Mor C1 ) } by CAT_6:def 17;
then consider f being morphism of C1 such that
A3: ( a = f & f is identity & f in Mor C1 ) ;
f |> f by A3, CAT_6:24;
then A4: ( T1 . f |> F1 . f & F2 . f |> T1 . f & T1 . f = (T1 . f) (*) (F1 . f) & T1 . f = (F2 . f) (*) (T1 . f) ) by A2, Th58, A3;
reconsider g = T1 . f as morphism of C2 ;
( F1 is identity-preserving & F2 is identity-preserving ) by CAT_6:def 25;
then A5: ( dom (T1 . f) = F1 . f & cod (T1 . f) = F2 . f ) by A4, CAT_6:26, CAT_6:27, A3, CAT_6:def 22;
A6: T1 . f = T1 . a by A3, CAT_6:def 21
.= T . a by A1, FUNCT_1:49 ;
( F1 . f = F1 . a & F2 . f = F2 . a ) by A3, CAT_6:def 21;
hence T . a in Hom ((F1 . a),(F2 . a)) by A6, A5, CAT_7:20; :: thesis:

end;

let a1, a2 be Object of C1; :: thesis:
let f be Morphism of a1,a2; :: thesis:
assume Hom (a1,a2) <> {} ; :: thesis:
then f in Hom (a1,a2) by CAT_7:def 3;
then f in { g where g is morphism of C1 : ex f1, f2 being morphism of C1 st
( a1 = f1 & a2 = f2 & g |> f1 & f2 |> g ) } by CAT_7:def 1;
then consider g being morphism of C1 such that
A7: ( f = g & ex f1, f2 being morphism of C1 st
( a1 = f1 & a2 = f2 & g |> f1 & f2 |> g ) ) ;
consider f1, f2 being morphism of C1 such that
A8: ( a1 = f1 & a2 = f2 & g |> f1 & f2 |> g ) by A7;
( f1 is identity & f2 is identity ) by A8, CAT_6:22;
then A9: ( T1 . f2 |> F1 . f & F2 . f |> T1 . f1 & T1 . f = (T1 . f2) (*) (F1 . f) & T1 . f = (F2 . f) (*) (T1 . f1) ) by A2, Th58, A8, A7;
A10: T1 . f2 = T1 . a2 by A8, CAT_6:def 21
.= T . a2 by A1, FUNCT_1:49 ;
T1 . f1 = T1 . a1 by A8, CAT_6:def 21
.= T . a1 by A1, FUNCT_1:49 ;
hence (T . a2) (*) (F1 . f) = (F2 . f) (*) (T . a1) by A9, A10; :: thesis:

end;

assume A11: for a being Object of C1 holds T . a in Hom ((F1 . a),(F2 . a)) ; :: thesis:
assume A12: for a1, a2 being Object of C1
for f being Morphism of a1,a2 st Hom (a1,a2) <> {} holds
(T . a2) (*) (F1 . f) = (F2 . f) (*) (T . a1) ; :: thesis:
defpred S₁[ object , object ] means for f being morphism of C1 st $1 = f holds
$2 = (T . (cod f)) (*) (F1 . f);
A13: for x being object st x in the carrier of C1 holds
ex y being object st
( y in the carrier of C2 & S₁[x,y] )

proof

let x be object ; :: thesis:
assume x in the carrier of C1 ; :: thesis:
then reconsider f = x as morphism of C1 by CAT_6:def 1;
reconsider y = (T . (cod f)) (*) (F1 . f) as object ;
take y ; :: thesis:
y in Mor C2 ;
hence y in the carrier of C2 by CAT_6:def 1; :: thesis:
thus S₁[x,y] ; :: thesis:

end;

consider T1 being Function of the carrier of C1, the carrier of C2 such that
A14: for x being object st x in the carrier of C1 holds
S₁[x,T1 . x] from FUNCT_2:sch 1(A13);
reconsider T1 = T1 as Functor of C1,C2 ;
take T1 ; :: thesis:
A15: dom T1 = the carrier of C1 by FUNCT_2:def 1
.= Mor C1 by CAT_6:def 1 ;
A16: dom T = Ob C1 by FUNCT_2:def 1
.= dom (T1 | (Ob C1)) by A15, RELAT_1:62 ;
for x being object st x in dom T holds
T . x = (T1 | (Ob C1)) . x

proof

let x be object ; :: thesis:
assume A17: x in dom T ; :: thesis:
then A18: x in Ob C1 ;
x in Mor C1 by A18;
then A19: x in the carrier of C1 by CAT_6:def 1;
reconsider f = x as morphism of C1 by A18;
A20: F1 is identity-preserving by CAT_6:def 25;
A21: f is identity by A17, CAT_6:22;
A22: F1 . f is identity by A17, CAT_6:22, A20, CAT_6:def 22;
T . (cod f) in Hom ((F1 . (cod f)),(F2 . (cod f))) by A11;
then dom (T . (cod f)) = F1 . (cod f) by CAT_7:20;
then dom (T . (cod f)) = cod (F1 . f) by CAT_6:32;
then A23: T . (cod f) |> F1 . f by CAT_7:5;
A24: cod f = x by A21, CAT_7:6;
T1 . x = (T . (cod f)) (*) (F1 . f) by A19, A14
.= T . x by A24, A23, A22, Th4 ;
hence T . x = (T1 | (Ob C1)) . x by A17, FUNCT_1:49; :: thesis:

end;

hence A25: T = T1 | (Ob C1) by A16, FUNCT_1:2; :: thesis:
for f, f1, f2 being morphism of C1 st f1 is identity & f2 is identity & f1 |> f & f |> f2 holds
( T1 . f1 |> F1 . f & F2 . f |> T1 . f2 & T1 . f = (T1 . f1) (*) (F1 . f) & T1 . f = (F2 . f) (*) (T1 . f2) )

proof

let f, f1, f2 be morphism of C1; :: thesis:
assume A26: ( f1 is identity & f2 is identity ) ; :: thesis:
assume A27: ( f1 |> f & f |> f2 ) ; :: thesis:
reconsider o1 = f1 as Object of C1 by A26, CAT_6:22;
T . o1 in Hom ((F1 . o1),(F2 . o1)) by A11;
then dom (T . o1) = F1 . o1 by CAT_7:20;
then dom (T . o1) = F1 . (cod f1) by A26, CAT_7:6;
then dom (T . o1) = cod (F1 . f1) by CAT_6:32;
then A28: T . o1 |> F1 . f1 by CAT_7:5;
A29: F1 . f1 |> F1 . f by A27, Th13;
A30: F1 . f1 is identity by A26, CAT_6:def 22, CAT_6:def 25;
A31: T . o1 = T1 . o1 by A25, FUNCT_1:49
.= T1 . f1 by CAT_6:def 21 ;
hence T1 . f1 |> F1 . f by A28, A29, A30, CAT_7:3; :: thesis:
reconsider o2 = f2 as Object of C1 by A26, CAT_6:22;
T . o2 in Hom ((F1 . o2),(F2 . o2)) by A11;
then cod (T . o2) = F2 . o2 by CAT_7:20;
then cod (T . o2) = F2 . (dom f2) by A26, CAT_7:6;
then cod (T . o2) = dom (F2 . f2) by CAT_6:32;
then A32: F2 . f2 |> T . o2 by CAT_7:5;
A33: F2 . f |> F2 . f2 by A27, Th13;
A34: F2 . f2 is identity by A26, CAT_6:def 22, CAT_6:def 25;
A35: T . o2 = T1 . o2 by A25, FUNCT_1:49
.= T1 . f2 by CAT_6:def 21 ;
hence F2 . f |> T1 . f2 by A32, A33, A34, CAT_7:3; :: thesis:
reconsider x = f as object ;
f in Mor C1 ;
then x in the carrier of C1 by CAT_6:def 1;
then A36: T1 . x = (T . (cod f)) (*) (F1 . f) by A14
.= (T1 . f1) (*) (F1 . f) by A31, A26, A27, CAT_6:def 19 ;
hence T1 . f = (T1 . f1) (*) (F1 . f) by CAT_6:def 21; :: thesis:
( dom f = o2 & cod f = o1 ) by A26, A27, CAT_6:def 18, CAT_6:def 19;
then A37: f in Hom (o2,o1) by CAT_7:20;
then reconsider g = f as Morphism of o2,o1 by CAT_7:def 3;
(T . o1) (*) (F1 . g) = (F2 . g) (*) (T . o2) by A37, A12;
hence T1 . f = (F2 . f) (*) (T1 . f2) by A36, A31, A35, CAT_6:def 21; :: thesis:

end;

hence T1 is_natural_transformation_of F1,F2 by Th58; :: thesis: