let C, D be Category; :: thesis: 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; :: thesis: 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; :: thesis: ( ( 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) ; :: thesis: T is Functor of C,D

now

thus for c being Object of C ex d being Object of D st T . (id c) = id d :: thesis: for f being Morphism of C holds
( T . (id (dom f)) = id (dom (T . f)) & T . (id (cod f)) = id (cod (T . f)) )

proof

let c be Object of C; :: thesis: ex d being Object of D st T . (id c) = id d
take F . c ; :: thesis: T . (id c) = id (F . c)
thus T . (id c) = id (F . c) by A1; :: thesis: verum

end;

thus for f being Morphism of C holds
( T . (id (dom f)) = id (dom (T . f)) & T . (id (cod f)) = id (cod (T . f)) ) :: thesis: verum

proof

let f be Morphism of C; :: thesis: ( T . (id (dom f)) = id (dom (T . f)) & T . (id (cod f)) = id (cod (T . f)) )
thus T . (id (dom f)) = id (F . (dom f)) by A1
.= id (dom (T . f)) by A2 ; :: thesis: T . (id (cod f)) = id (cod (T . f))
thus T . (id (cod f)) = id (F . (cod f)) by A1
.= id (cod (T . f)) by A2 ; :: thesis: verum

end;

end;

hence T is Functor of C,D by A3, Th96; :: thesis: verum