let f be NtoSEG Function of (Segm 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 object ; :: 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 A1: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 ) ; :: thesis: x1 = x2
reconsider x1 = x1, x2 = x2 as Element of Segm n by A1;
Segm (x1 + 1) = succ (Segm x1) by NAT_1:38
.= ntoSeg x1
.= f . x2 by A1, Def5
.= ntoSeg x2 by Def5
.= succ (Segm x2)
.= Segm (x2 + 1) by NAT_1:38 ;
hence x1 = x2 ; :: thesis: verum

end;

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