let n be Element of NAT ; ( S3[n] implies S3[n + 1] )
assume A1:
S3[n]
; S3[n + 1]
let v1, v2 be FinSequence of REAL ; ( len v1 = n + 1 & len v2 = n + 1 & rng v1 = rng v2 & v1 is increasing & v2 is increasing implies v1 = v2 )
assume that
A2:
len v1 = n + 1
and
A3:
len v2 = n + 1
and
A4:
rng v1 = rng v2
and
A5:
v1 is increasing
and
A6:
v2 is increasing
; v1 = v2
reconsider X = rng v1 as Subset of REAL ;
set u = upper_bound X;
X <> {}
by A2, CARD_1:47, RELAT_1:64;
then A8:
upper_bound X in X
by Th1;
then consider m being Nat such that
A9:
m in dom v2
and
A10:
v2 . m = upper_bound X
by A4, FINSEQ_2:11;
reconsider m = m as Element of NAT by ORDINAL1:def 13;
A11:
m <= len v2
by A9, FINSEQ_3:27;
A12:
n <= n + 1
by NAT_1:11;
then
Seg n c= Seg (n + 1)
by FINSEQ_1:7;
then A13:
Seg n = (Seg (n + 1)) /\ (Seg n)
by XBOOLE_1:28;
dom v2 = Seg (len v2)
by FINSEQ_1:def 3;
then A14:
dom (v2 | (Seg n)) = Seg n
by A3, A13, RELAT_1:90;
dom v1 = Seg (len v1)
by FINSEQ_1:def 3;
then A15:
dom (v1 | (Seg n)) = Seg n
by A2, A13, RELAT_1:90;
then reconsider f1 = v1 | (Seg n), f2 = v2 | (Seg n) as FinSequence by A14, FINSEQ_1:def 2;
rng f2 c= rng v2
by RELAT_1:99;
then A16:
rng f2 c= REAL
by XBOOLE_1:1;
rng f1 c= rng v1
by RELAT_1:99;
then
rng f1 c= REAL
by XBOOLE_1:1;
then reconsider f1 = f1, f2 = f2 as FinSequence of REAL by A16, FINSEQ_1:def 4;
consider k being Nat such that
A17:
k in dom v1
and
A18:
v1 . k = upper_bound X
by A8, FINSEQ_2:11;
reconsider k = k as Element of NAT by ORDINAL1:def 13;
A19:
k <= len v1
by A17, FINSEQ_3:27;
A20:
1 <= k
by A17, FINSEQ_3:27;
A25:
1 <= m
by A9, FINSEQ_3:27;
A30:
len f1 = n
by A15, FINSEQ_1:def 3;
then A31:
dom f1 c= dom v1
by A2, A12, FINSEQ_3:32;
A32:
rng f1 = (rng v1) \ {(upper_bound X)}
proof
thus
rng f1 c= (rng v1) \ {(upper_bound X)}
XBOOLE_0:def 10 (rng v1) \ {(upper_bound X)} c= rng f1proof
let x be
set ;
TARSKI:def 3 ( not x in rng f1 or x in (rng v1) \ {(upper_bound X)} )
assume
x in rng f1
;
x in (rng v1) \ {(upper_bound X)}
then consider i being
Nat such that A33:
i in dom f1
and A34:
f1 . i = x
by FINSEQ_2:11;
A35:
x = v1 . i
by A33, A34, FUNCT_1:70;
A36:
v1 . i in rng v1
by A31, A33, FUNCT_1:def 5;
i <= n
by A15, A33, FINSEQ_1:3;
then
i <> n + 1
by NAT_1:13;
then
x <> upper_bound X
by A2, A5, A17, A18, A21, A31, A33, A35, Th19;
then
not
x in {(upper_bound X)}
by TARSKI:def 1;
hence
x in (rng v1) \ {(upper_bound X)}
by A35, A36, XBOOLE_0:def 5;
verum
end;
let x be
set ;
TARSKI:def 3 ( not x in (rng v1) \ {(upper_bound X)} or x in rng f1 )
assume A37:
x in (rng v1) \ {(upper_bound X)}
;
x in rng f1
then
x in rng v1
by XBOOLE_0:def 5;
then consider i being
Nat such that A38:
i in dom v1
and A39:
v1 . i = x
by FINSEQ_2:11;
A40:
i <= len v1
by A38, FINSEQ_3:27;
not
x in {(upper_bound X)}
by A37, XBOOLE_0:def 5;
then
i <> len v1
by A18, A21, A39, TARSKI:def 1;
then
i < len v1
by A40, XXREAL_0:1;
then A41:
i <= len f1
by A2, A30, NAT_1:13;
1
<= i
by A38, FINSEQ_3:27;
then A42:
i in dom f1
by A41, FINSEQ_3:27;
then
f1 . i in rng f1
by FUNCT_1:def 5;
hence
x in rng f1
by A39, A42, FUNCT_1:70;
verum
end;
A43:
dom v1 = Seg (len v1)
by FINSEQ_1:def 3;
len (f1 ^ <*(upper_bound X)*>) =
n + (len <*(upper_bound X)*>)
by A30, FINSEQ_1:35
.=
len v1
by A2, FINSEQ_1:56
;
then A49:
v1 = f1 ^ <*(upper_bound X)*>
by A44, FINSEQ_2:10;
A50:
len f2 = n
by A14, FINSEQ_1:def 3;
then A51: len (f2 ^ <*(upper_bound X)*>) =
n + (len <*(upper_bound X)*>)
by FINSEQ_1:35
.=
len v2
by A3, FINSEQ_1:56
;
A52:
dom f2 c= dom v2
by A3, A12, A50, FINSEQ_3:32;
A53:
rng f2 = (rng v2) \ {(upper_bound X)}
proof
thus
rng f2 c= (rng v2) \ {(upper_bound X)}
XBOOLE_0:def 10 (rng v2) \ {(upper_bound X)} c= rng f2proof
let x be
set ;
TARSKI:def 3 ( not x in rng f2 or x in (rng v2) \ {(upper_bound X)} )
assume
x in rng f2
;
x in (rng v2) \ {(upper_bound X)}
then consider i being
Nat such that A54:
i in dom f2
and A55:
f2 . i = x
by FINSEQ_2:11;
A56:
x = v2 . i
by A54, A55, FUNCT_1:70;
A57:
v2 . i in rng v2
by A52, A54, FUNCT_1:def 5;
i <= n
by A14, A54, FINSEQ_1:3;
then
i <> n + 1
by NAT_1:13;
then
x <> upper_bound X
by A3, A6, A9, A10, A26, A52, A54, A56, Th19;
then
not
x in {(upper_bound X)}
by TARSKI:def 1;
hence
x in (rng v2) \ {(upper_bound X)}
by A56, A57, XBOOLE_0:def 5;
verum
end;
let x be
set ;
TARSKI:def 3 ( not x in (rng v2) \ {(upper_bound X)} or x in rng f2 )
assume A58:
x in (rng v2) \ {(upper_bound X)}
;
x in rng f2
then
x in rng v2
by XBOOLE_0:def 5;
then consider i being
Nat such that A59:
i in dom v2
and A60:
v2 . i = x
by FINSEQ_2:11;
A61:
i <= len v2
by A59, FINSEQ_3:27;
not
x in {(upper_bound X)}
by A58, XBOOLE_0:def 5;
then
i <> len v2
by A10, A26, A60, TARSKI:def 1;
then
i < len v2
by A61, XXREAL_0:1;
then A62:
i <= len f2
by A3, A50, NAT_1:13;
1
<= i
by A59, FINSEQ_3:27;
then A63:
i in dom f2
by A62, FINSEQ_3:27;
then
f2 . i in rng f2
by FUNCT_1:def 5;
hence
x in rng f2
by A60, A63, FUNCT_1:70;
verum
end;
A64:
dom v2 = Seg (len v2)
by FINSEQ_1:def 3;
( f1 is increasing & f2 is increasing )
by A5, A6, Th20;
then
f1 = f2
by A1, A4, A30, A50, A32, A53;
hence
v1 = v2
by A49, A51, A65, FINSEQ_2:10; verum