let C, D be Category; :: thesis:
let T be Function of the carrier' of C, the carrier' of D; :: thesis:
let F be Function of the carrier of C, the carrier of D; :: thesis:
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:
A4: for c being Object of C ex d being Object of D st T . (id c) = id d

let c be Object of C; :: thesis:
take F . c ; :: thesis:
thus T . (id c) = id (F . c) by A1; :: thesis:

end;

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

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

end;