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

A11: now

let a be object of ; :: thesis: F . a = G . a
thus F . a = a by A7
.= G . a by A9 ; :: thesis: verum

end;

now

let a, b be object of ; :: thesis: ( <^a,b^> <> {} implies for f being Morphism of , holds F . f = G . f )
assume A12: <^a,b^> <> {} ; :: thesis: for f being Morphism of , holds F . f = G . f
let f be Morphism of ,; :: 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