consider F being contravariant Functor of F₁(),F₂() such that
A5: for a being Object of F₁() holds F . a = F₃(a) and
A6: for a, b being Object of F₁() st <^a,b^> <> {} holds
for f being Morphism of a,b holds F . f = F₄(a,b,f) by A1;
A7: for a, b being Object of F₁() st F₃(a) = F₃(b) holds
a = b by A2;
A8: for a, b being Object of F₁() st <^a,b^> <> {} holds
for f, g being Morphism of a,b st F₄(a,b,f) = F₄(a,b,g) holds
f = g by A3;
A9: for a, b being Object of F₂() st <^a,b^> <> {} holds
for f being Morphism of a,b ex c, d being Object of F₁() ex g being Morphism of c,d st
( b = F₃(c) & a = F₃(d) & <^c,d^> <> {} & f = F₄(c,d,g) ) by A4;
take F ; :: according to FUNCTOR0:def 40 :: thesis: ( F is bijective & F is contravariant )
thus F is bijective from YELLOW18:sch 12(A5, A6, A7, A8, A9); :: thesis: F is contravariant
thus F is contravariant ; :: thesis: verum