theorem Th44:
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]] ) )