let C, D be Category; for T being Function of the carrier' of C, the carrier' of D st ( 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)) ) ) & ( 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 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)) ) ) & ( 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 ex d being Object of D st T . (id c) = id d
and
A2:
for f being Morphism of C holds
( T . (id (dom f)) = id (dom (T . f)) & T . (id (cod f)) = id (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
thus
for c being Element of C ex d being Element of D st T . (id c) = id d
by A1; CAT_1:def 21 ( ( for f being Element of the carrier' of C holds
( T . (id (dom f)) = id (dom (T . f)) & T . (id (cod f)) = id (cod (T . f)) ) ) & ( for f, g being Element of the carrier' of C st [g,f] in dom the Comp of C holds
T . (g (*) f) = (T . g) (*) (T . f) ) )
thus
for f being Element of the carrier' of C holds
( T . (id (dom f)) = id (dom (T . f)) & T . (id (cod f)) = id (cod (T . f)) )
by A2; for f, g being Element of the carrier' of C st [g,f] in dom the Comp of C holds
T . (g (*) f) = (T . g) (*) (T . f)
let f, g be Element of the carrier' of C; ( [g,f] in dom the Comp of C implies T . (g (*) f) = (T . g) (*) (T . f) )
assume
[g,f] in dom the Comp of C
; T . (g (*) f) = (T . g) (*) (T . f)
then A4:
dom g = cod f
by Def4;
thus
T . (g (*) f) = (T . g) (*) (T . f)
by A3, A4; verum