for A being category
for a, b being Object of A st <^a,b^> <> {} holds
for f being Morphism of a,b ex F being Function of ((Concretized A) -carrier_of a),((Concretized A) -carrier_of b) st
( F in the Arrows of (Concretized A) . (a,b) & ( for c being Object of A
for g being Morphism of c,a st <^c,a^> <> {} holds
F . [g,[c,a]] = [(f * g),[c,b]] ) )