thus ex F being strict contravariant Functor of A,B st
( ( for a being Object of A holds F . a = H₁(a) ) & ( for a, b being Object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds F . f = H₂(a,b,f) ) ) from YELLOW18:sch 9(A2, A3, A5, A6); :: thesis: verum