let X0 be finite natural-membered set ; :: thesis: ex m being Nat st X0 c= m
A1: X0 c= NAT by MEMBERED:6;
consider p being Function such that
A2: ( rng p = X0 & dom p in NAT ) by FINSET_1:def 1;
reconsider np = dom p as Element of NAT by A2;
np = dom p ;
then reconsider p = p as XFinSequence by AFINSQ_1:7;
reconsider p = p as XFinSequence of NAT by A1, A2, ORDINAL1:def 8;
defpred S₁[ Nat] means ex n being Nat st
for i being Nat st i in $1 & $1 -' 1 in dom p holds
p . i in n;
for i being Nat st i in 0 & 0 -' 1 in dom p holds
p . i in 0 ;
then A4: S₁[ 0 ] ;
A6: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume S₁[k] ; :: thesis: S₁[k + 1]
then consider n being Nat such that
B1: for i being Nat st i in k & k -' 1 in dom p holds
p . i in n ;

per cases ( (k + 1) - 1 < len p or (k + 1) - 1 >= len p ) ;

suppose C0: (k + 1) - 1 < len p ; :: thesis: S₁[k + 1]

k -' 1 <= k by NAT_D:35;
then k -' 1 < len p by C0, XXREAL_0:2;
then C2: k -' 1 in dom p by NAT_1:45;
set m = p . k;
set m2 = max n,((p . k) + 1);
for i being Nat st i in k + 1 & (k + 1) -' 1 in dom p holds
p . i in max n,((p . k) + 1)

proof

let i be Nat; :: thesis: ( i in k + 1 & (k + 1) -' 1 in dom p implies p . i in max n,((p . k) + 1) )
assume ( i in k + 1 & (k + 1) -' 1 in dom p ) ; :: thesis: p . i in max n,((p . k) + 1)
then D2: i < k + 1 by NAT_1:45;

per cases ( i < k or i >= k ) ;

suppose i < k ; :: thesis: p . i in max n,((p . k) + 1)

then i in k by NAT_1:45;
then E2: p . i in n by B1, C2;
set k0 = p . i;
p . i < n by E2, NAT_1:45;
then p . i < max n,((p . k) + 1) by XXREAL_0:30;
hence p . i in max n,((p . k) + 1) by NAT_1:45; :: thesis: verum

end;

suppose E0: i >= k ; :: thesis: p . i in max n,((p . k) + 1)

i <= k by D2, NAT_1:13;
then E2: p . i = p . k by E0, XXREAL_0:1;
p . k < (p . k) + 1 by XREAL_1:31;
then p . k < max n,((p . k) + 1) by XXREAL_0:30;
hence p . i in max n,((p . k) + 1) by E2, NAT_1:45; :: thesis: verum

end;

end;

end;

hence S₁[k + 1] ; :: thesis: verum

end;

suppose E20: (k + 1) - 1 >= len p ; :: thesis: S₁[k + 1]

E30: (k + 1) -' 1 = k by NAT_D:34;
for i being Nat st i in k + 1 & (k + 1) -' 1 in dom p holds
p . i in 2 by E20, E30, NAT_1:45;
hence S₁[k + 1] ; :: thesis: verum

end;

end;

end;

for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A4, A6);
then consider n being Nat such that
A5: for i being Nat st i in len p & (len p) -' 1 in dom p holds
p . i in n ;
rng p c= n

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng p or y in n )
assume y in rng p ; :: thesis: y in n
then consider x being set such that
B2: ( x in dom p & y = p . x ) by FUNCT_1:def 5;
reconsider nn = dom p as Nat ;
reconsider nx = x as Nat by B2;
B6: (len p) - 1 < len p by XREAL_1:46;
0 + 1 <= len p by B2, NAT_1:13;
then (len p) -' 1 = (len p) - 1 by XREAL_1:235;
then ( nx in len p & (len p) -' 1 in dom p ) by B2, B6, NAT_1:45;
hence y in n by B2, A5; :: thesis: verum

end;

hence ex m being Nat st X0 c= m by A2; :: thesis: verum