:: deftheorem defines ?- ISOCAT_2:def 3 :
for A, B, C being Category
for F being Functor of [:A,B:],C
for f being Morphism of A holds F ?- f = (curry (F,f)) * (IdMap B);