let n be non zero Nat; :: thesis: for f being NtoSEG Function of (Segm n),(Seg n) holds rng f = Seg n
let f be NtoSEG Function of (Segm n),(Seg n); :: thesis: rng f = Seg n
A1: dom f = n by FUNCT_2:def 1;

now :: thesis: for x being object st x in Seg n holds
x in rng f

let x be object ; :: thesis: ( x in Seg n implies x in rng f )
assume x in Seg n ; :: thesis: x in rng f
then consider xk being Nat such that
A2: ( x = xk & 1 <= xk & xk <= n ) ;
( xk - 1 is Element of NAT & xk - 1 < n ) by A2, NAT_1:21, XREAL_1:147;
then reconsider i = xk - 1 as Element of Segm n by NAT_1:44;
f . i = ntoSeg i by Def5
.= succ (Segm i)
.= Segm (i + 1) by NAT_1:38 ;
hence x in rng f by A1, A2, FUNCT_1:def 3; :: thesis: verum

end;

then Seg n c= rng f by TARSKI:def 3;
hence rng f = Seg n by XBOOLE_0:def 10; :: thesis: verum