theorem Th34: :: YELLOW18:34

for C being para-functional category
for a, b being Object of C st <^a,b^> <> {} holds
for f being Morphism of a,b holds f is Function of (the_carrier_of a),(the_carrier_of b)