let f be NtoSEG Function of n,(Seg n); :: thesis: f is bijective
thus f is one-to-one :: according to FUNCT_2:def 4 :: thesis: f is onto

proof

let x1, x2 be set ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in proj1 f or not x2 in proj1 f or not f . x1 = f . x2 or x1 = x2 )
assume ASL1: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 ) ; :: thesis: x1 = x2
reconsider x1 = x1, x2 = x2 as Element of n by ASL1;
( f . x1 = ntoSeg x1 & f . x2 = ntoSeg x2 ) by defNtoSEG;
then x1 + 1 = x2 + 1 by ASL1;
hence x1 = x2 ; :: thesis: verum

end;

thus rng f = Seg n by RNGNtoSEG; :: according to FUNCT_2:def 3 :: thesis: verum