let C, D be Category; :: thesis: 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; :: thesis: ( ( 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) ; :: thesis: T is Functor of C,D
thus for c being Element of the carrier of C ex d being Element of the carrier of D st T . (the Id of C . c) = the Id of D . d :: according to CAT_1:def 18 :: thesis: ( ( for f being Element of the carrier' of C holds
( T . (the Id of C . (the Source of C . f)) = the Id of D . (the Source of D . (T . f)) & T . (the Id of C . (the Target of C . f)) = the Id of D . (the Target of D . (T . f)) ) ) & ( for f, g being Element of the carrier' of C st [g,f] in dom the Comp of C holds
T . (the Comp of C . g,f) = the Comp of D . (T . g),(T . f) ) )

proof

let c be Element of the carrier of C; :: thesis: ex d being Element of the carrier of D st T . (the Id of C . c) = the Id of D . d
consider d being Object of D such that
A4: T . (id c) = id d by A1;
thus ex d being Element of the carrier of D st T . (the Id of C . c) = the Id of D . d by A4; :: thesis: verum

end;

thus for f being Element of the carrier' of C holds
( T . (the Id of C . (the Source of C . f)) = the Id of D . (the Source of D . (T . f)) & T . (the Id of C . (the Target of C . f)) = the Id of D . (the Target of D . (T . f)) ) :: thesis: for f, g being Element of the carrier' of C st [g,f] in dom the Comp of C holds
T . (the Comp of C . g,f) = the Comp of D . (T . g),(T . f)

proof

let f be Element of the carrier' of C; :: thesis: ( T . (the Id of C . (the Source of C . f)) = the Id of D . (the Source of D . (T . f)) & T . (the Id of C . (the Target of C . f)) = the Id of D . (the Target of D . (T . f)) )
( the Source of C . f = dom f & the Id of C . (dom f) = id (dom f) & the Source of D . (T . f) = dom (T . f) & the Id of D . (dom (T . f)) = id (dom (T . f)) & the Target of C . f = cod f & the Id of C . (cod f) = id (cod f) & the Target of D . (T . f) = cod (T . f) & the Id of D . (cod (T . f)) = id (cod (T . f)) ) ;
hence ( T . (the Id of C . (the Source of C . f)) = the Id of D . (the Source of D . (T . f)) & T . (the Id of C . (the Target of C . f)) = the Id of D . (the Target of D . (T . f)) ) by A2; :: thesis: verum

end;

let f, g be Element of the carrier' of C; :: thesis: ( [g,f] in dom the Comp of C implies T . (the Comp of C . g,f) = the Comp of D . (T . g),(T . f) )
assume [g,f] in dom the Comp of C ; :: thesis: T . (the Comp of C . g,f) = the Comp of D . (T . g),(T . f)
then A5: dom g = cod f by Def8;
then id (dom (T . g)) = T . (id (cod f)) by A2
.= id (cod (T . f)) by A2 ;
then ( the Comp of C . g,f = g * f & the Comp of D . (T . g),(T . f) = (T . g) * (T . f) ) by A5, Th41, Th45;
hence T . (the Comp of C . g,f) = the Comp of D . (T . g),(T . f) by A3, A5; :: thesis: verum