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
A6: for a being object of A holds F . a = a and
A7: for a, b being object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds F . f = f and
A8: for a being object of A holds G . a = a and
A9: 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

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

end;

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