let C, D be Category; for T being Function of the carrier' of C, the carrier' of D
for F being Function of the carrier of C, the carrier of D st ( for c being Object of C holds T . (id c) = id (F . c) ) & ( for f being Morphism of C holds
( F . (dom f) = dom (T . f) & F . (cod f) = cod (T . f) ) ) & ( for f, g being Morphism of C st dom g = cod f holds
T . (g (*) f) = (T . g) (*) (T . f) ) holds
T is Functor of C,D
let T be Function of the carrier' of C, the carrier' of D; for F being Function of the carrier of C, the carrier of D st ( for c being Object of C holds T . (id c) = id (F . c) ) & ( for f being Morphism of C holds
( F . (dom f) = dom (T . f) & F . (cod f) = cod (T . f) ) ) & ( for f, g being Morphism of C st dom g = cod f holds
T . (g (*) f) = (T . g) (*) (T . f) ) holds
T is Functor of C,D
let F be Function of the carrier of C, the carrier of D; ( ( for c being Object of C holds T . (id c) = id (F . c) ) & ( for f being Morphism of C holds
( F . (dom f) = dom (T . f) & F . (cod f) = cod (T . f) ) ) & ( for f, g being Morphism of C st dom g = cod f holds
T . (g (*) f) = (T . g) (*) (T . f) ) implies T is Functor of C,D )
assume that
A1:
for c being Object of C holds T . (id c) = id (F . c)
and
A2:
for f being Morphism of C holds
( F . (dom f) = dom (T . f) & F . (cod f) = cod (T . f) )
and
A3:
for f, g being Morphism of C st dom g = cod f holds
T . (g (*) f) = (T . g) (*) (T . f)
; T is Functor of C,D
A4:
for c being Object of C ex d being Object of D st T . (id c) = id d
for f being Morphism of C holds
( T . (id (dom f)) = id (dom (T . f)) & T . (id (cod f)) = id (cod (T . f)) )
hence
T is Functor of C,D
by A3, A4, Th56; verum