let n be Nat; ( S2[n] implies S2[n + 1] )
assume A1:
S2[n]
; S2[n + 1]
let v be FinSequence of REAL ; ( card (rng v) = n + 1 implies ex v1 being FinSequence of REAL st
( rng v1 = rng v & len v1 = card (rng v) & v1 is increasing ) )
assume A2:
card (rng v) = n + 1
; ex v1 being FinSequence of REAL st
( rng v1 = rng v & len v1 = card (rng v) & v1 is increasing )
now ex v1 being FinSequence of REAL st
( rng v1 = rng v & len v1 = card (rng v) & v1 is increasing )reconsider R =
rng v as
finite Subset of
REAL ;
set u =
upper_bound R;
set X =
R \ {(upper_bound R)};
set f =
(R \ {(upper_bound R)}) |` v;
(
Seq ((R \ {(upper_bound R)}) |` v) = ((R \ {(upper_bound R)}) |` v) * (Sgm (dom ((R \ {(upper_bound R)}) |` v))) &
rng (Sgm (dom ((R \ {(upper_bound R)}) |` v))) = dom ((R \ {(upper_bound R)}) |` v) )
by FINSEQ_1:50;
then A3:
rng (Seq ((R \ {(upper_bound R)}) |` v)) =
rng ((R \ {(upper_bound R)}) |` v)
by RELAT_1:28
.=
R \ {(upper_bound R)}
by RELAT_1:89, XBOOLE_1:36
;
then reconsider f1 =
Seq ((R \ {(upper_bound R)}) |` v) as
FinSequence of
REAL by FINSEQ_1:def 4;
reconsider X =
R \ {(upper_bound R)} as
finite set ;
upper_bound R in R
by A2, Th132, CARD_1:27;
then A4:
{(upper_bound R)} c= R
by ZFMISC_1:31;
then A5:
card X = (card R) - (card {(upper_bound R)})
by CARD_2:44;
A6:
card {(upper_bound R)} = 1
by CARD_1:30;
then consider v2 being
FinSequence of
REAL such that A7:
rng v2 = rng f1
and A8:
len v2 = card (rng f1)
and A9:
v2 is
increasing
by A1, A2, A3, A5;
reconsider uu =
upper_bound R as
Element of
REAL by XREAL_0:def 1;
take v1 =
v2 ^ <*uu*>;
( rng v1 = rng v & len v1 = card (rng v) & v1 is increasing )thus rng v1 =
X \/ (rng <*(upper_bound R)*>)
by A3, A7, FINSEQ_1:31
.=
((rng v) \ {(upper_bound R)}) \/ {(upper_bound R)}
by FINSEQ_1:39
.=
(rng v) \/ {(upper_bound R)}
by XBOOLE_1:39
.=
rng v
by A4, XBOOLE_1:12
;
( len v1 = card (rng v) & v1 is increasing )thus A10:
len v1 =
n + (len <*(upper_bound R)*>)
by A2, A3, A5, A6, A8, FINSEQ_1:22
.=
card (rng v)
by A2, FINSEQ_1:39
;
v1 is increasing now for k, m being Nat st k in dom v1 & m in dom v1 & k < m holds
v1 . k < v1 . mlet k,
m be
Nat;
( k in dom v1 & m in dom v1 & k < m implies v1 . k < v1 . m )assume that A11:
k in dom v1
and A12:
m in dom v1
and A13:
k < m
;
v1 . k < v1 . mA14:
1
<= m
by A12, FINSEQ_3:25;
A15:
m <= len v1
by A12, FINSEQ_3:25;
set r =
v1 . k;
set s =
v1 . m;
A16:
1
<= k
by A11, FINSEQ_3:25;
A17:
k <= len v1
by A11, FINSEQ_3:25;
now v1 . k < v1 . mper cases
( m = len v1 or m <> len v1 )
;
suppose A18:
m = len v1
;
v1 . k < v1 . m
k < len v1
by A13, A15, XXREAL_0:2;
then
k <= len v2
by A2, A3, A5, A6, A8, A10, NAT_1:13;
then A19:
k in dom v2
by A16, FINSEQ_3:25;
then
v1 . k = v2 . k
by FINSEQ_1:def 7;
then A20:
v1 . k in rng v2
by A19, FUNCT_1:def 3;
then
v1 . k in R
by A3, A7, XBOOLE_0:def 5;
then A21:
v1 . k <= upper_bound R
by Def1;
not
v1 . k in {(upper_bound R)}
by A3, A7, A20, XBOOLE_0:def 5;
then A22:
v1 . k <> upper_bound R
by TARSKI:def 1;
v1 . m = upper_bound R
by A2, A3, A5, A6, A8, A10, A18, FINSEQ_1:42;
hence
v1 . k < v1 . m
by A21, A22, XXREAL_0:1;
verum end; suppose
m <> len v1
;
v1 . k < v1 . mthen
m < len v1
by A15, XXREAL_0:1;
then
m <= len v2
by A2, A3, A5, A6, A8, A10, NAT_1:13;
then A23:
m in dom v2
by A14, FINSEQ_3:25;
then A24:
v1 . m = v2 . m
by FINSEQ_1:def 7;
k < len v1
by A13, A17, A15, XXREAL_0:1;
then
k <= len v2
by A2, A3, A5, A6, A8, A10, NAT_1:13;
then A25:
k in dom v2
by A16, FINSEQ_3:25;
then
v1 . k = v2 . k
by FINSEQ_1:def 7;
hence
v1 . k < v1 . m
by A9, A13, A25, A23, A24, SEQM_3:def 1;
verum end; hence
v1 . k < v1 . m
;
verum end; hence
v1 is
increasing
by SEQM_3:def 1;
verum end;
hence
ex v1 being FinSequence of REAL st
( rng v1 = rng v & len v1 = card (rng v) & v1 is increasing )
; verum