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 ) holds
for c being Object of C
for d being Object of D st T . (id c) = id d holds
(Obj T) . 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 ) implies for c being Object of C
for d being Object of D st T . (id c) = id d holds
(Obj T) . c = d )
assume A1: for c being Object of C ex d being Object of D st T . (id c) = id d ; :: thesis: for c being Object of C
for d being Object of D st T . (id c) = id d holds
(Obj T) . c = d
A2: for c being Element of C ex d being Element of D st T . (the Id of C . c) = the Id of D . d

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
consider d being Object of D such that
A3: T . (id c) = id d by A1;
take d ; :: thesis: T . (the Id of C . c) = the Id of D . d
thus T . (the Id of C . c) = the Id of D . d by A3; :: thesis: verum

end;

let c be Object of C; :: thesis: for d being Object of D st T . (id c) = id d holds
(Obj T) . c = d
let d be Object of D; :: thesis: ( T . (id c) = id d implies (Obj T) . c = d )
thus ( T . (id c) = id d implies (Obj T) . c = d ) by A2, Def19; :: thesis: verum