:: deftheorem defines para-functional YELLOW18:def 7 :
for C being category holds
( C is para-functional iff ex F being ManySortedSet of C st
for a1, a2 being Object of C holds <^a1,a2^> c= Funcs ((F . a1),(F . a2)) );