ex F being Functor of F₁(),F₂() st
for f being Morphism of F₁() holds F . f = F₄(f)

A1: for f being Morphism of F₁() holds
( F₄(f) is Morphism of F₂() & ( for g being Morphism of F₂() st g = F₄(f) holds
( dom g = F₃((dom f)) & cod g = F₃((cod f)) ) ) ) and
A2: for a being Object of F₁() holds F₄((id a)) = id F₃(a) and
A3: for f1, f2 being Morphism of F₁()
for g1, g2 being Morphism of F₂() st g1 = F₄(f1) & g2 = F₄(f2) & dom f2 = cod f1 holds
F₄((f2 (*) f1)) = g2 (*) g1