theorem Th33: :: YELLOW18:33

for C being category holds
( C is para-functional iff for a1, a2 being Object of C holds <^a1,a2^> c= Funcs ((the_carrier_of a1),(the_carrier_of a2)) )