theorem Th35: :: YELLOW18:35

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
( dom f = the_carrier_of a & rng f c= the_carrier_of b )