ex F being strict covariant Functor of F₁(),F₂() st
( ( for a being Object of F₁() holds F . a = F₃(a) ) & ( 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) ) )

A1: for a being Object of F₁() holds F₃(a) is Object of F₂() and
A2: for a, b being Object of F₁() st <^a,b^> <> {} holds
for f being Morphism of a,b holds F₄(a,b,f) in the Arrows of F₂() . (F₃(a),F₃(b)) and
A3: for a, b, c being Object of F₁() st <^a,b^> <> {} & <^b,c^> <> {} holds
for f being Morphism of a,b
for g being Morphism of b,c
for a9, b9, c9 being Object of F₂() st a9 = F₃(a) & b9 = F₃(b) & c9 = F₃(c) holds
for f9 being Morphism of a9,b9
for g9 being Morphism of b9,c9 st f9 = F₄(a,b,f) & g9 = F₄(b,c,g) holds
F₄(a,c,(g * f)) = g9 * f9 and
A4: for a being Object of F₁()
for a9 being Object of F₂() st a9 = F₃(a) holds
F₄(a,a,(idm a)) = idm a9