let F, G be strict contravariant Functor of A,B; ( ( 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
; F = G
hence
F = G
by A11, Th2; verum