:: deftheorem Def2 defines " ISOCAT_1:def 2 :
for A, B being Category
for F being Functor of A,B st F is isomorphic holds
F " = F " ;