consider F being contravariant Functor of F₁(),F₂() such that
A5: for a being object of holds F . a = F₃(a) and
A6: for a, b being object of st <^a,b^> <> {} holds
for f being Morphism of , holds F . f = F₄(a,b,f) by A1;
A7: for a, b being object of st F₃(a) = F₃(b) holds
a = b by A2;
A8: for a, b being object of st <^a,b^> <> {} holds
for f, g being Morphism of , st F₄(a,b,f) = F₄(a,b,g) holds
f = g by A3;
A9: for a, b being object of st <^a,b^> <> {} holds
for f being Morphism of , ex c, d being object of ex g being Morphism of , st
( b = F₃(c) & a = F₃(d) & <^c,d^> <> {} & f = F₄(c,d,g) ) by A4;
take F ; :: according to FUNCTOR0:def 41 :: 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