:: deftheorem defines surjective ENS_1:def 8 :
for V being non empty set
for m being Element of Maps V holds
( m is surjective iff rng (m `2) = cod m );