let F, G be strict contravariant Functor of A,B; :: 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 = f ) & ( 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 = f ) implies F = G )
assume that
A7: for a being Object of A holds F . a = a and
A8: for a, b being Object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds F . f = f and
A9: for a being Object of A holds G . a = a and
A10: for a, b being Object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds G . f = f ; :: thesis: F = G

A11: 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 A7
.= G . a by A9 ; :: 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 A12: <^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
thus F . f = f by A8, A12
.= G . f by A10, A12 ; :: thesis: verum

end;

hence F = G by A11, Th2; :: thesis: verum