let n be 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:27, RELAT_1:41;
then A7:
upper_bound X in X
by Th132;
then consider m being Nat such that
A8:
m in dom v2
and
A9:
v2 . m = upper_bound X
by A4, FINSEQ_2:10;
reconsider m = m as Element of NAT by ORDINAL1:def 12;
A10:
m <= len v2
by A8, FINSEQ_3:25;
A11:
n <= n + 1
by NAT_1:11;
then
Seg n c= Seg (n + 1)
by FINSEQ_1:5;
then A12:
Seg n = (Seg (n + 1)) /\ (Seg n)
by XBOOLE_1:28;
dom v2 = Seg (len v2)
by FINSEQ_1:def 3;
then A13:
dom (v2 | (Seg n)) = Seg n
by A3, A12, RELAT_1:61;
dom v1 = Seg (len v1)
by FINSEQ_1:def 3;
then A14:
dom (v1 | (Seg n)) = Seg n
by A2, A12, RELAT_1:61;
then reconsider f1 = v1 | (Seg n), f2 = v2 | (Seg n) as FinSequence by A13, FINSEQ_1:def 2;
rng f2 c= rng v2
by RELAT_1:70;
then A15:
rng f2 c= REAL
by XBOOLE_1:1;
rng f1 c= rng v1
by RELAT_1:70;
then
rng f1 c= REAL
by XBOOLE_1:1;
then reconsider f1 = f1, f2 = f2 as FinSequence of REAL by A15, FINSEQ_1:def 4;
consider k being Nat such that
A16:
k in dom v1
and
A17:
v1 . k = upper_bound X
by A7, FINSEQ_2:10;
reconsider k = k as Element of NAT by ORDINAL1:def 12;
A18:
k <= len v1
by A16, FINSEQ_3:25;
A19:
1 <= k
by A16, FINSEQ_3:25;
A24:
1 <= m
by A8, FINSEQ_3:25;
n in NAT
by ORDINAL1:def 12;
then A29:
len f1 = n
by A14, FINSEQ_1:def 3;
then A30:
dom f1 c= dom v1
by A2, A11, FINSEQ_3:30;
A31:
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
object ;
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 A32:
i in dom f1
and A33:
f1 . i = x
by FINSEQ_2:10;
A34:
x = v1 . i
by A32, A33, FUNCT_1:47;
A35:
v1 . i in rng v1
by A30, A32, FUNCT_1:def 3;
i <= n
by A14, A32, FINSEQ_1:1;
then
i <> n + 1
by NAT_1:13;
then
x <> upper_bound X
by A2, A5, A16, A17, A20, A30, A32, A34, Th137;
then
not
x in {(upper_bound X)}
by TARSKI:def 1;
hence
x in (rng v1) \ {(upper_bound X)}
by A34, A35, XBOOLE_0:def 5;
verum
end;
let x be
object ;
TARSKI:def 3 ( not x in (rng v1) \ {(upper_bound X)} or x in rng f1 )
assume A36:
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 A37:
i in dom v1
and A38:
v1 . i = x
by FINSEQ_2:10;
A39:
i <= len v1
by A37, FINSEQ_3:25;
not
x in {(upper_bound X)}
by A36, XBOOLE_0:def 5;
then
i <> len v1
by A17, A20, A38, TARSKI:def 1;
then
i < len v1
by A39, XXREAL_0:1;
then A40:
i <= len f1
by A2, A29, NAT_1:13;
1
<= i
by A37, FINSEQ_3:25;
then A41:
i in dom f1
by A40, FINSEQ_3:25;
then
f1 . i in rng f1
by FUNCT_1:def 3;
hence
x in rng f1
by A38, A41, FUNCT_1:47;
verum
end;
A42:
dom v1 = Seg (len v1)
by FINSEQ_1:def 3;
len (f1 ^ <*(upper_bound X)*>) =
n + (len <*(upper_bound X)*>)
by A29, FINSEQ_1:22
.=
len v1
by A2, FINSEQ_1:39
;
then A48:
v1 = f1 ^ <*(upper_bound X)*>
by A43, FINSEQ_2:9;
n in NAT
by ORDINAL1:def 12;
then A49:
len f2 = n
by A13, FINSEQ_1:def 3;
then A50: len (f2 ^ <*(upper_bound X)*>) =
n + (len <*(upper_bound X)*>)
by FINSEQ_1:22
.=
len v2
by A3, FINSEQ_1:39
;
A51:
dom f2 c= dom v2
by A3, A11, A49, FINSEQ_3:30;
A52:
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
object ;
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 A53:
i in dom f2
and A54:
f2 . i = x
by FINSEQ_2:10;
A55:
x = v2 . i
by A53, A54, FUNCT_1:47;
A56:
v2 . i in rng v2
by A51, A53, FUNCT_1:def 3;
i <= n
by A13, A53, FINSEQ_1:1;
then
i <> n + 1
by NAT_1:13;
then
x <> upper_bound X
by A3, A6, A8, A9, A25, A51, A53, A55, Th137;
then
not
x in {(upper_bound X)}
by TARSKI:def 1;
hence
x in (rng v2) \ {(upper_bound X)}
by A55, A56, XBOOLE_0:def 5;
verum
end;
let x be
object ;
TARSKI:def 3 ( not x in (rng v2) \ {(upper_bound X)} or x in rng f2 )
assume A57:
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 A58:
i in dom v2
and A59:
v2 . i = x
by FINSEQ_2:10;
A60:
i <= len v2
by A58, FINSEQ_3:25;
not
x in {(upper_bound X)}
by A57, XBOOLE_0:def 5;
then
i <> len v2
by A9, A25, A59, TARSKI:def 1;
then
i < len v2
by A60, XXREAL_0:1;
then A61:
i <= len f2
by A3, A49, NAT_1:13;
1
<= i
by A58, FINSEQ_3:25;
then A62:
i in dom f2
by A61, FINSEQ_3:25;
then
f2 . i in rng f2
by FUNCT_1:def 3;
hence
x in rng f2
by A59, A62, FUNCT_1:47;
verum
end;
A63:
dom v2 = Seg (len v2)
by FINSEQ_1:def 3;
( f1 is increasing & f2 is increasing )
by A5, A6;
then
f1 = f2
by A1, A4, A29, A49, A31, A52;
hence
v1 = v2
by A48, A50, A64, FINSEQ_2:9; verum