let X0 be finite natural-membered set ; :: thesis: ex n being Nat st X0 c= Segm n
consider p being Function such that
A1: rng p = X0 and
A2: 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:5;
X0 c= NAT by MEMBERED:6;
then reconsider p = p as XFinSequence of NAT by A1, RELAT_1:def 19;
defpred S1[ Nat] means ex n being Nat st
for i being Nat st i in Segm $1 & $1 -' 1 in dom p holds
p . i in n;
A3: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume S1[k] ; :: thesis: S1[k + 1]
then consider n being Nat such that
A4: 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 A5: (k + 1) - 1 < len p ; :: thesis: S1[k + 1]
set m = p . k;
set m2 = max (n,((p . k) + 1));
k -' 1 <= k by NAT_D:35;
then k -' 1 < len p by A5, XXREAL_0:2;
then A6: k -' 1 in dom p by AFINSQ_1:86;
for i being Nat st i in Segm (k + 1) & (k + 1) -' 1 in dom p holds
p . i in Segm (max (n,((p . k) + 1)))
proof
let i be Nat; :: thesis: ( i in Segm (k + 1) & (k + 1) -' 1 in dom p implies p . i in Segm (max (n,((p . k) + 1))) )
assume that
A7: i in Segm (k + 1) and
(k + 1) -' 1 in dom p ; :: thesis: p . i in Segm (max (n,((p . k) + 1)))
A8: i < k + 1 by A7, NAT_1:44;
per cases ( i < k or i >= k ) ;
suppose A9: i < k ; :: thesis: p . i in Segm (max (n,((p . k) + 1)))
set k0 = p . i;
i in Segm k by A9, NAT_1:44;
then p . i in Segm n by A4, A6;
then p . i < n by NAT_1:44;
hence p . i in Segm (max (n,((p . k) + 1))) by NAT_1:44, XXREAL_0:30; :: thesis: verum
end;
suppose A10: i >= k ; :: thesis: p . i in Segm (max (n,((p . k) + 1)))
p . k < (p . k) + 1 by XREAL_1:29;
then A11: p . k < max (n,((p . k) + 1)) by XXREAL_0:30;
i <= k by A8, NAT_1:13;
then p . i = p . k by A10, XXREAL_0:1;
hence p . i in Segm (max (n,((p . k) + 1))) by A11, NAT_1:44; :: thesis: verum
end;
end;
end;
hence S1[k + 1] ; :: thesis: verum
end;
suppose A12: (k + 1) - 1 >= len p ; :: thesis: S1[k + 1]
(k + 1) -' 1 = k by NAT_D:34;
then for i being Nat st i in k + 1 & (k + 1) -' 1 in dom p holds
p . i in 2 by A12, AFINSQ_1:86;
hence S1[k + 1] ; :: thesis: verum
end;
end;
end;
for i being Nat st i in 0 & 0 -' 1 in dom p holds
p . i in 0 ;
then A13: S1[ 0 ] ;
for k being Nat holds S1[k] from NAT_1:sch 2(A13, A3);
 then consider n being Nat such that
A14: for i being Nat st i in Segm (len p) & (len p) -' 1 in dom p holds
p . i in n ;
rng p c= Segm n
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng p or y in Segm n )
assume y in rng p ; :: thesis: y in Segm n
then consider x being object such that
A15: x in dom p and
A16: y = p . x by FUNCT_1:def 3;
A17: (len p) - 1 < len p by XREAL_1:44;
0 < len p by A15;
then 0 + 1 <= len p by NAT_1:13;
then (len p) -' 1 = (len p) - 1 by XREAL_1:233;
then (len p) -' 1 in dom p by A17, AFINSQ_1:86;
hence y in Segm n by A14, A15, A16; :: thesis: verum
end;
hence ex n being Nat st X0 c= Segm n by A1; :: thesis: verum