defpred S1[ Nat] means for X being set st X c= Segm $1 holds
ex p being XFinSequence of NAT st
( rng p = X & ( for l, m, k1, k2 being Nat st l < m & m < len p & k1 = p . l & k2 = p . m holds
k1 < k2 ) );
A1:
ex k being Nat st X c= Segm k
by Th2;
A2:
for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume A3:
for
X being
set st
X c= Segm k holds
ex
p being
XFinSequence of
NAT st
(
rng p = X & ( for
l,
m,
k1,
k2 being
Nat st
l < m &
m < len p &
k1 = p . l &
k2 = p . m holds
k1 < k2 ) )
;
S1[k + 1]
let X be
set ;
( X c= Segm (k + 1) implies ex p being XFinSequence of NAT st
( rng p = X & ( for l, m, k1, k2 being Nat st l < m & m < len p & k1 = p . l & k2 = p . m holds
k1 < k2 ) ) )
assume A4:
X c= Segm (k + 1)
;
ex p being XFinSequence of NAT st
( rng p = X & ( for l, m, k1, k2 being Nat st l < m & m < len p & k1 = p . l & k2 = p . m holds
k1 < k2 ) )
now ( not X c= k implies ex p being XFinSequence of NAT st
( rng p = X & ( for l, m, k1, k2 being Nat st l < m & m < len p & k1 = p . l & k2 = p . m holds
k1 < k2 ) ) )set Y =
X \ {k};
assume
not
X c= k
;
ex p being XFinSequence of NAT st
( rng p = X & ( for l, m, k1, k2 being Nat st l < m & m < len p & k1 = p . l & k2 = p . m holds
k1 < k2 ) )then consider x being
object such that A5:
x in X
and A6:
not
x in Segm k
;
reconsider n =
x as
Element of
NAT by A4, A5, Th1;
n < k + 1
by A4, A5, NAT_1:44;
then A7:
n <= k
by NAT_1:13;
not
n < k
by A6, NAT_1:44;
then A8:
n = k
by A7, XXREAL_0:1;
A9:
X \ {k} c= Segm k
then consider p being
XFinSequence of
NAT such that A13:
rng p = X \ {k}
and A14:
for
l,
m,
k1,
k2 being
Nat st
l < m &
m < len p &
k1 = p . l &
k2 = p . m holds
k1 < k2
by A3;
reconsider k =
k as
Element of
NAT by ORDINAL1:def 12;
consider q being
XFinSequence of
NAT such that A15:
q = p ^ <%k%>
;
A16:
for
l,
m,
k1,
k2 being
Nat st
l < m &
m < len q &
k1 = q . l &
k2 = q . m holds
k1 < k2
proof
let l,
m,
k1,
k2 be
Nat;
( l < m & m < len q & k1 = q . l & k2 = q . m implies k1 < k2 )
assume that A17:
l < m
and A18:
m < len q
and A19:
k1 = q . l
and A20:
k2 = q . m
;
k1 < k2
m + 1
<= len q
by A18, NAT_1:13;
then A21:
m <= (len q) - 1
by XREAL_1:19;
then
l < (len (p ^ <%k%>)) - 1
by A15, A17, XXREAL_0:2;
then
l < ((len p) + (len <%k%>)) - 1
by AFINSQ_1:17;
then
l < ((len p) + 1) - 1
by AFINSQ_1:34;
then A22:
l in dom p
by AFINSQ_1:86;
A23:
m <= (len q) -' 1
by A21, XREAL_0:def 2;
A24:
now ( m <> (len q) -' 1 implies k1 < k2 )A25:
k1 = p . l
by A15, A19, A22, AFINSQ_1:def 3;
assume
m <> (len q) -' 1
;
k1 < k2then
m < (len (p ^ <%k%>)) -' 1
by A15, A23, XXREAL_0:1;
then
m < ((len p) + (len <%k%>)) -' 1
by AFINSQ_1:17;
then
m < ((len p) + 1) -' 1
by AFINSQ_1:34;
then A26:
m < len p
by NAT_D:34;
then
m in dom p
by AFINSQ_1:86;
then
k2 = p . m
by A15, A20, AFINSQ_1:def 3;
hence
k1 < k2
by A14, A17, A26, A25;
verum end;
hence
k1 < k2
by A24;
verum
end; A28:
{k} c= X
by A5, A8, ZFMISC_1:31;
rng q =
(rng p) \/ (rng <%k%>)
by A15, AFINSQ_1:26
.=
(X \ {k}) \/ {k}
by A13, AFINSQ_1:33
.=
X \/ {k}
by XBOOLE_1:39
.=
X
by A28, XBOOLE_1:12
;
hence
ex
p being
XFinSequence of
NAT st
(
rng p = X & ( for
l,
m,
k1,
k2 being
Nat st
l < m &
m < len p &
k1 = p . l &
k2 = p . m holds
k1 < k2 ) )
by A16;
verum end;
hence
ex
p being
XFinSequence of
NAT st
(
rng p = X & ( for
l,
m,
k1,
k2 being
Nat st
l < m &
m < len p &
k1 = p . l &
k2 = p . m holds
k1 < k2 ) )
by A3;
verum
end;
A29:
S1[ 0 ]
proof
let X be
set ;
( X c= Segm 0 implies ex p being XFinSequence of NAT st
( rng p = X & ( for l, m, k1, k2 being Nat st l < m & m < len p & k1 = p . l & k2 = p . m holds
k1 < k2 ) ) )
assume A30:
X c= Segm 0
;
ex p being XFinSequence of NAT st
( rng p = X & ( for l, m, k1, k2 being Nat st l < m & m < len p & k1 = p . l & k2 = p . m holds
k1 < k2 ) )
take
<%> NAT
;
( rng (<%> NAT) = X & ( for l, m, k1, k2 being Nat st l < m & m < len (<%> NAT) & k1 = (<%> NAT) . l & k2 = (<%> NAT) . m holds
k1 < k2 ) )
thus
rng (<%> NAT) = X
by A30;
for l, m, k1, k2 being Nat st l < m & m < len (<%> NAT) & k1 = (<%> NAT) . l & k2 = (<%> NAT) . m holds
k1 < k2
thus
for
l,
m,
k1,
k2 being
Nat st
l < m &
m < len (<%> NAT) &
k1 = (<%> NAT) . l &
k2 = (<%> NAT) . m holds
k1 < k2
;
verum
end;
for k2 being Nat holds S1[k2]
from NAT_1:sch 2(A29, A2);
hence
ex b1 being XFinSequence of NAT st
( rng b1 = X & ( for l, m, k1, k2 being Nat st l < m & m < len b1 & k1 = b1 . l & k2 = b1 . m holds
k1 < k2 ) )
by A1; verum