:: deftheorem Def5 defines NtoSEG DESCIP_1:def 5 :
for n being non zero Nat
for f being Function of (Segm n),(Seg n) holds
( f is NtoSEG iff for i being Element of Segm n holds f . i = ntoSeg i );