let n be Nat; :: thesis: ( S3[n] implies S3[n + 1] )
assume A1: S3[n] ; :: thesis: S3[n + 1]
let v1, v2 be FinSequence of REAL ; :: thesis: ( 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 ; :: thesis: 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;
A20: now :: thesis: not k <> len v1
assume k <> len v1 ; :: thesis: contradiction
then k < len v1 by A18, XXREAL_0:1;
then A21: k + 1 <= len v1 by NAT_1:13;
reconsider s = v1 . (k + 1) as Real ;
A22: k < k + 1 by NAT_1:13;
1 <= k + 1 by A19, NAT_1:13;
then A23: k + 1 in dom v1 by A21, FINSEQ_3:25;
then v1 . (k + 1) in rng v1 by FUNCT_1:def 3;
then s <= upper_bound X by Def1;
hence contradiction by A5, A16, A17, A23, A22, SEQM_3:def 1; :: thesis: verum
end;
A24: 1 <= m by A8, FINSEQ_3:25;
A25: now :: thesis: not m <> len v2
assume m <> len v2 ; :: thesis: contradiction
then m < len v2 by A10, XXREAL_0:1;
then A26: m + 1 <= len v2 by NAT_1:13;
reconsider s = v2 . (m + 1) as Real ;
A27: m < m + 1 by NAT_1:13;
1 <= m + 1 by A24, NAT_1:13;
then A28: m + 1 in dom v2 by A26, FINSEQ_3:25;
then v2 . (m + 1) in rng v2 by FUNCT_1:def 3;
then s <= upper_bound X by A4, Def1;
hence contradiction by A6, A8, A9, A28, A27, SEQM_3:def 1; :: thesis: verum
end;
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)} :: according to XBOOLE_0:def 10 :: thesis: (rng v1) \ {(upper_bound X)} c= rng f1
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng f1 or x in (rng v1) \ {(upper_bound X)} )
assume x in rng f1 ; :: thesis: 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; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (rng v1) \ {(upper_bound X)} or x in rng f1 )
assume A36: x in (rng v1) \ {(upper_bound X)} ; :: thesis: 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; :: thesis: verum
end;
A42: dom v1 = Seg (len v1) by FINSEQ_1:def 3;
A43: now :: thesis: for i being Nat st i in dom v1 holds
(f1 ^ <*(upper_bound X)*>) . i = v1 . i
let i be Nat; :: thesis: ( i in dom v1 implies (f1 ^ <*(upper_bound X)*>) . i = v1 . i )
assume A44: i in dom v1 ; :: thesis: (f1 ^ <*(upper_bound X)*>) . i = v1 . i
then A45: 1 <= i by A42, FINSEQ_1:1;
A46: i <= (len f1) + 1 by A2, A29, A42, A44, FINSEQ_1:1;
now :: thesis: (f1 ^ <*(upper_bound X)*>) . i = v1 . i
per cases ( i = (len f1) + 1 or i <> (len f1) + 1 ) ;
suppose i = (len f1) + 1 ; :: thesis: (f1 ^ <*(upper_bound X)*>) . i = v1 . i
hence (f1 ^ <*(upper_bound X)*>) . i = v1 . i by A2, A17, A20, A29, FINSEQ_1:42; :: thesis: verum
end;
suppose i <> (len f1) + 1 ; :: thesis: (f1 ^ <*(upper_bound X)*>) . i = v1 . i
then i < (len f1) + 1 by A46, XXREAL_0:1;
then i <= len f1 by NAT_1:13;
then A47: i in dom f1 by A14, A29, A45;
hence (f1 ^ <*(upper_bound X)*>) . i = f1 . i by FINSEQ_1:def 7
.= v1 . i by A47, FUNCT_1:47 ;
:: thesis: verum
end;
end;
end;
hence (f1 ^ <*(upper_bound X)*>) . i = v1 . i ; :: thesis: verum
end;
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)} :: according to XBOOLE_0:def 10 :: thesis: (rng v2) \ {(upper_bound X)} c= rng f2
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng f2 or x in (rng v2) \ {(upper_bound X)} )
assume x in rng f2 ; :: thesis: 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; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (rng v2) \ {(upper_bound X)} or x in rng f2 )
assume A57: x in (rng v2) \ {(upper_bound X)} ; :: thesis: 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; :: thesis: verum
end;
A63: dom v2 = Seg (len v2) by FINSEQ_1:def 3;
A64: now :: thesis: for i being Nat st i in dom v2 holds
(f2 ^ <*(upper_bound X)*>) . i = v2 . i
let i be Nat; :: thesis: ( i in dom v2 implies (f2 ^ <*(upper_bound X)*>) . i = v2 . i )
assume A65: i in dom v2 ; :: thesis: (f2 ^ <*(upper_bound X)*>) . i = v2 . i
then A66: 1 <= i by A63, FINSEQ_1:1;
A67: i <= (len f2) + 1 by A3, A49, A63, A65, FINSEQ_1:1;
now :: thesis: (f2 ^ <*(upper_bound X)*>) . i = v2 . i
per cases ( i = (len f2) + 1 or i <> (len f2) + 1 ) ;
suppose i = (len f2) + 1 ; :: thesis: (f2 ^ <*(upper_bound X)*>) . i = v2 . i
hence (f2 ^ <*(upper_bound X)*>) . i = v2 . i by A3, A9, A25, A49, FINSEQ_1:42; :: thesis: verum
end;
suppose i <> (len f2) + 1 ; :: thesis: (f2 ^ <*(upper_bound X)*>) . i = v2 . i
then i < (len f2) + 1 by A67, XXREAL_0:1;
then i <= len f2 by NAT_1:13;
then A68: i in dom f2 by A13, A49, A66;
hence (f2 ^ <*(upper_bound X)*>) . i = f2 . i by FINSEQ_1:def 7
.= v2 . i by A68, FUNCT_1:47 ;
:: thesis: verum
end;
end;
end;
hence (f2 ^ <*(upper_bound X)*>) . i = v2 . i ; :: thesis: verum
end;
( f1 is increasing & f2 is increasing ) by A5, A6, Th138;
then f1 = f2 by A1, A4, A29, A49, A31, A52;
hence v1 = v2 by A48, A50, A64, FINSEQ_2:9; :: thesis: verum