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

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

let x be set ; :: thesis: ( x in Seg n implies x in rng f )
assume x in Seg n ; :: thesis: x in rng f
then consider xk being Element of NAT such that
T1: ( x = xk & 1 <= xk & xk <= n ) ;
( xk - 1 is Element of NAT & xk - 1 < n ) by T1, NAT_1:21, XREAL_1:147;
then reconsider i = xk - 1 as Element of n by NAT_1:44;
f . i = ntoSeg i by defNtoSEG;
hence x in rng f by L1, T1, 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