A5: for a, b being object of F₁() st F₃(a) = F₃(b) holds
a = b by A2;
A6: 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;
A7: 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
( a = F₃(c) & b = F₃(d) & <^c,d^> <> {} & f = F₄(c,d,g) ) by A4;
consider F being covariant Functor of F₁(),F₂() such that
A8: for a being object of F₁() holds F . a = F₃(a) and
A9: 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;
take F ; :: according to FUNCTOR0:def 40 :: thesis: ( F is bijective & F is covariant )
thus F is bijective from YELLOW18:sch 10(A8, A9, A5, A6, A7); :: thesis: F is covariant
thus F is covariant ; :: thesis: verum