let n be Element of NAT ; :: thesis: ( S2[n] implies S2[n + 1] )
assume A1:
S2[n]
; :: thesis: S2[n + 1]
let v be FinSequence of REAL ; :: thesis: ( 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
; :: thesis: ex v1 being FinSequence of REAL st
( rng v1 = rng v & len v1 = card (rng v) & v1 is increasing )
now reconsider R =
rng v as
finite Subset of
REAL by FINSEQ_1:def 4;
A3:
(
R is
bounded_above &
upper_bound R in R )
by A2, Th1, CARD_1:47;
set u =
upper_bound R;
set X =
R \ {(upper_bound R)};
reconsider f =
(R \ {(upper_bound R)}) | v as
FinSubsequence by FINSEQ_1:69;
(
R \ {(upper_bound R)} c= REAL &
Seq f = f * (Sgm (dom f)) &
rng (Sgm (dom f)) = dom f )
by FINSEQ_1:71, FINSEQ_1:def 14;
then A4:
rng (Seq f) =
rng f
by RELAT_1:47
.=
R \ {(upper_bound R)}
by RELAT_1:120, XBOOLE_1:36
;
then reconsider f1 =
Seq f as
FinSequence of
REAL by FINSEQ_1:def 4;
reconsider X =
R \ {(upper_bound R)} as
finite set ;
A5:
{(upper_bound R)} c= R
by A3, ZFMISC_1:37;
then A6:
(
card X = (card R) - (card {(upper_bound R)}) &
card {(upper_bound R)} = 1 )
by CARD_1:50, CARD_2:63;
then consider v2 being
FinSequence of
REAL such that A7:
(
rng v2 = rng f1 &
len v2 = card (rng f1) &
v2 is
increasing )
by A1, A2, A4;
take v1 =
v2 ^ <*(upper_bound R)*>;
:: thesis: ( rng v1 = rng v & len v1 = card (rng v) & v1 is increasing )thus rng v1 =
X \/ (rng <*(upper_bound R)*>)
by A4, A7, FINSEQ_1:44
.=
((rng v) \ {(upper_bound R)}) \/ {(upper_bound R)}
by FINSEQ_1:56
.=
(rng v) \/ {(upper_bound R)}
by XBOOLE_1:39
.=
rng v
by A5, XBOOLE_1:12
;
:: thesis: ( len v1 = card (rng v) & v1 is increasing )thus A8:
len v1 =
n + (len <*(upper_bound R)*>)
by A2, A4, A6, A7, FINSEQ_1:35
.=
card (rng v)
by A2, FINSEQ_1:56
;
:: thesis: v1 is increasing now let k,
m be
Element of
NAT ;
:: thesis: ( k in dom v1 & m in dom v1 & k < m implies v1 . k < v1 . m )assume A9:
(
k in dom v1 &
m in dom v1 &
k < m )
;
:: thesis: v1 . k < v1 . mthen A10:
( 1
<= k &
k <= len v1 & 1
<= m &
m <= len v1 )
by FINSEQ_3:27;
set r =
v1 . k;
set s =
v1 . m;
now per cases
( m = len v1 or m <> len v1 )
;
suppose
m = len v1
;
:: thesis: v1 . k < v1 . mthen A11:
v1 . m = upper_bound R
by A2, A4, A6, A7, A8, FINSEQ_1:59;
k < len v1
by A9, A10, XXREAL_0:2;
then
k <= len v2
by A2, A4, A6, A7, A8, NAT_1:13;
then A12:
k in dom v2
by A10, FINSEQ_3:27;
then
v1 . k = v2 . k
by FINSEQ_1:def 7;
then
v1 . k in rng v2
by A12, FUNCT_1:def 5;
then
(
v1 . k in R & not
v1 . k in {(upper_bound R)} )
by A4, A7, XBOOLE_0:def 5;
then
(
v1 . k <= upper_bound R &
v1 . k <> upper_bound R )
by SEQ_4:def 4, TARSKI:def 1;
hence
v1 . k < v1 . m
by A11, XXREAL_0:1;
:: thesis: verum end; suppose
m <> len v1
;
:: thesis: v1 . k < v1 . mthen
(
m < len v1 &
k < len v1 )
by A9, A10, XXREAL_0:1;
then
(
k <= len v2 &
m <= len v2 )
by A2, A4, A6, A7, A8, NAT_1:13;
then A13:
(
k in dom v2 &
m in dom v2 )
by A10, FINSEQ_3:27;
then
(
v1 . k = v2 . k &
v1 . m = v2 . m )
by FINSEQ_1:def 7;
hence
v1 . k < v1 . m
by A7, A9, A13, SEQM_3:def 1;
:: thesis: verum end; hence
v1 . k < v1 . m
;
:: thesis: verum end; hence
v1 is
increasing
by SEQM_3:def 1;
:: thesis: verum end;
hence
ex v1 being FinSequence of REAL st
( rng v1 = rng v & len v1 = card (rng v) & v1 is increasing )
; :: thesis: verum