:: deftheorem Def10 defines fCod ENS_1:def 10 :
for V being non empty set
for b₂ being Function of (Maps V),V holds
( b₂ = fCod V iff for m being Element of Maps V holds b₂ . m = cod m );