:: deftheorem defines cod ENS_1:def 4 :
for V being non empty set
for m being Element of Maps V holds cod m = (m `1) `2 ;