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 C ex d being Element of D st T . ( the Id of C . c) = the Id of D . d :: according to CAT_1:def 15 :: 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 C; :: thesis: ex d being Element of D st T . ( the Id of C . c) = the Id of D . d
ex d being Object of D st T . (id c) = id d by A1;
hence ex d being Element of D st T . ( the Id of C . c) = the Id of D . d ; :: 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)) )
A4: ( the Id of C . (cod f) = id (cod f) & the Id of D . (cod (T . f)) = id (cod (T . f)) ) ;
( the Id of C . (dom f) = id (dom f) & the Id of D . (dom (T . f)) = id (dom (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, A4; :: 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 A6: the Comp of D . ((T . g),(T . f)) = (T . g) * (T . f) by Th41, Th45;
the Comp of C . (g,f) = g * f by A5, Th41;
hence T . ( the Comp of C . (g,f)) = the Comp of D . ((T . g),(T . f)) by A3, A5, A6; :: thesis: verum