:: deftheorem defines @ ENS_1:def 17 :
for V being non empty set
for f being Morphism of (Ens V) holds @ f = f;