theorem
for
C1,
C2 being non
empty category for
F1,
F2 being
covariant Functor of
C1,
C2 for
T being
Function of
(Ob C1),
(Mor C2) holds
( ex
T1 being
Functor of
C1,
C2 st
(
T = T1 | (Ob C1) &
T1 is_natural_transformation_of F1,
F2 ) iff ( ( for
a being
Object of
C1 holds
T . a in Hom (
(F1 . a),
(F2 . a)) ) & ( 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) ) ) )