let F, G be strict covariant Functor of A, Concretized A; :: thesis: ( ( for a being Object of A holds F . a = a ) & ( for a, b being Object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds (F . f) . [(idm a),[a,a]] = [f,[a,b]] ) & ( for a being Object of A holds G . a = a ) & ( for a, b being Object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds (G . f) . [(idm a),[a,a]] = [f,[a,b]] ) implies F = G )
assume that
A1: for a being Object of A holds F . a = a and
A2: for a, b being Object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds (F . f) . [(idm a),[a,a]] = [f,[a,b]] and
A3: for a being Object of A holds G . a = a and
A4: for a, b being Object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds (G . f) . [(idm a),[a,a]] = [f,[a,b]] ; :: thesis: F = G

A5: now :: thesis: for a being Object of A holds F . a = G . a

let a be Object of A; :: thesis: F . a = G . a
thus F . a = a by A1
.= G . a by A3 ; :: thesis: verum

end;

now :: thesis: for a, b being Object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds F . f = G . f

let a, b be Object of A; :: thesis: ( <^a,b^> <> {} implies for f being Morphism of a,b holds F . f = G . f )
assume A6: <^a,b^> <> {} ; :: thesis: for f being Morphism of a,b holds F . f = G . f
let f be Morphism of a,b; :: thesis: F . f = G . f
A7: (F . f) . [(idm a),[a,a]] = [f,[a,b]] by A2, A6;
A8: (G . f) . [(idm a),[a,a]] = [f,[a,b]] by A4, A6;
A9: <^(F . a),(F . b)^> <> {} by A6, FUNCTOR0:def 18;
A10: F . a = a by A1;
A11: F . b = b by A1;
A12: G . a = a by A3;
G . b = b by A3;
hence F . f = G . f by A7, A8, A9, A10, A11, A12, Th45; :: thesis: verum

end;

hence F = G by A5, Th1; :: thesis: verum