:: deftheorem defines Ens ENS_1:def 13 :
for V being non empty set holds Ens V = CatStr(# V,(Maps V),(fDom V),(fCod V),(fComp V) #);