let n be Element of 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 A2: ( len v1 = n + 1 & len v2 = n + 1 & rng v1 = rng v2 & v1 is increasing & v2 is increasing ) ; :: thesis: v1 = v2
A3: ( dom v1 = Seg (len v1) & dom v2 = Seg (len v2) & rng v1 c= REAL ) by FINSEQ_1:def 3, FINSEQ_1:def 4;
reconsider X = rng v1 as Subset of REAL by FINSEQ_1:def 4;
X <> {} by A2, CARD_1:47, RELAT_1:64;
then A4: ( X is bounded_above & upper_bound X in X ) by Th1;
set u = upper_bound X;
consider k being Nat such that
A5: ( k in dom v1 & v1 . k = upper_bound X ) by A4, FINSEQ_2:11;
reconsider k = k as Element of NAT by ORDINAL1:def 13;
A6: ( 1 <= k & k <= len v1 ) by A5, FINSEQ_3:27;
A7: now
assume k <> len v1 ; :: thesis: contradiction
then ( k < len v1 & k <= k + 1 ) by A6, NAT_1:11, XXREAL_0:1;
then ( 1 <= k + 1 & k + 1 <= len v1 ) by A6, NAT_1:13;
then A8: k + 1 in dom v1 by FINSEQ_3:27;
then A9: v1 . (k + 1) in rng v1 by FUNCT_1:def 5;
reconsider s = v1 . (k + 1) as Real ;
A10: s <= upper_bound X by A9, SEQ_4:def 4;
k < k + 1 by NAT_1:13;
hence contradiction by A2, A5, A8, A10, SEQM_3:def 1; :: thesis: verum
end;
consider m being Nat such that
A11: ( m in dom v2 & v2 . m = upper_bound X ) by A2, A4, FINSEQ_2:11;
reconsider m = m as Element of NAT by ORDINAL1:def 13;
A12: ( 1 <= m & m <= len v2 ) by A11, FINSEQ_3:27;
A13: now
assume m <> len v2 ; :: thesis: contradiction
then ( m < len v2 & m <= m + 1 ) by A12, NAT_1:11, XXREAL_0:1;
then ( 1 <= m + 1 & m + 1 <= len v2 ) by A12, NAT_1:13;
then A14: m + 1 in dom v2 by FINSEQ_3:27;
then A15: v2 . (m + 1) in rng v2 by FUNCT_1:def 5;
reconsider s = v2 . (m + 1) as Real ;
A16: s <= upper_bound X by A2, A15, SEQ_4:def 4;
m < m + 1 by NAT_1:13;
hence contradiction by A2, A11, A14, A16, SEQM_3:def 1; :: thesis: verum
end;
A17: n <= n + 1 by NAT_1:11;
then Seg n c= Seg (n + 1) by FINSEQ_1:7;
then Seg n = (Seg (n + 1)) /\ (Seg n) by XBOOLE_1:28;
then A18: ( dom (v1 | (Seg n)) = Seg n & dom (v2 | (Seg n)) = Seg n ) by A2, A3, RELAT_1:90;
then reconsider f1 = v1 | (Seg n), f2 = v2 | (Seg n) as FinSequence by FINSEQ_1:def 2;
( rng f1 c= rng v1 & rng f2 c= rng v2 ) by RELAT_1:99;
then ( rng f1 c= REAL & rng f2 c= REAL ) by A2, A3, XBOOLE_1:1;
then reconsider f1 = f1, f2 = f2 as FinSequence of REAL by FINSEQ_1:def 4;
A19: ( len f1 = n & len f2 = n ) by A18, FINSEQ_1:def 3;
then A20: dom f1 c= dom v1 by A2, A17, FINSEQ_3:32;
A21: 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 set ; :: 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
A22: ( i in dom f1 & f1 . i = x ) by FINSEQ_2:11;
A23: ( 1 <= i & i <= n & x = v1 . i ) by A18, A22, FINSEQ_1:3, FUNCT_1:70;
then ( i <> n + 1 & i in dom v1 & n + 1 in Seg (len v1) ) by A2, A20, A22, FINSEQ_1:6, NAT_1:13;
then x <> upper_bound X by A2, A5, A7, A23, Th19;
then ( not x in {(upper_bound X)} & v1 . i in rng v1 ) by A20, A22, FUNCT_1:def 5, TARSKI:def 1;
hence x in (rng v1) \ {(upper_bound X)} by A23, XBOOLE_0:def 5; :: thesis: verum
end;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (rng v1) \ {(upper_bound X)} or x in rng f1 )
assume A24: x in (rng v1) \ {(upper_bound X)} ; :: thesis: x in rng f1
then A25: ( x in rng v1 & not x in {(upper_bound X)} ) by XBOOLE_0:def 5;
consider i being Nat such that
A26: ( i in dom v1 & v1 . i = x ) by A24, FINSEQ_2:11;
A27: i <> len v1 by A5, A7, A25, A26, TARSKI:def 1;
A28: ( 1 <= i & i <= len v1 ) by A26, FINSEQ_3:27;
then i < len v1 by A27, XXREAL_0:1;
then i <= len f1 by A2, A19, NAT_1:13;
then i in dom f1 by A28, FINSEQ_3:27;
then ( f1 . i in rng f1 & f1 . i = v1 . i ) by FUNCT_1:70, FUNCT_1:def 5;
hence x in rng f1 by A26; :: thesis: verum
end;
A29: dom f2 c= dom v2 by A2, A17, A19, FINSEQ_3:32;
A30: 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 set ; :: 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
A31: ( i in dom f2 & f2 . i = x ) by FINSEQ_2:11;
A32: ( 1 <= i & i <= n & x = v2 . i ) by A18, A31, FINSEQ_1:3, FUNCT_1:70;
then ( i <> n + 1 & i in dom v2 & n + 1 in Seg (len v2) ) by A2, A29, A31, FINSEQ_1:6, NAT_1:13;
then x <> upper_bound X by A2, A11, A13, A32, Th19;
then ( not x in {(upper_bound X)} & v2 . i in rng v2 ) by A29, A31, FUNCT_1:def 5, TARSKI:def 1;
hence x in (rng v2) \ {(upper_bound X)} by A32, XBOOLE_0:def 5; :: thesis: verum
end;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (rng v2) \ {(upper_bound X)} or x in rng f2 )
assume A33: x in (rng v2) \ {(upper_bound X)} ; :: thesis: x in rng f2
then A34: ( x in rng v2 & not x in {(upper_bound X)} ) by XBOOLE_0:def 5;
consider i being Nat such that
A35: ( i in dom v2 & v2 . i = x ) by A33, FINSEQ_2:11;
A36: i <> len v2 by A11, A13, A34, A35, TARSKI:def 1;
A37: ( 1 <= i & i <= len v2 ) by A35, FINSEQ_3:27;
then i < len v2 by A36, XXREAL_0:1;
then i <= len f2 by A2, A19, NAT_1:13;
then i in dom f2 by A37, FINSEQ_3:27;
then ( f2 . i in rng f2 & f2 . i = v2 . i ) by FUNCT_1:70, FUNCT_1:def 5;
hence x in rng f2 by A35; :: thesis: verum
end;
( f1 is increasing & f2 is increasing ) by A2, Th20;
then A38: f1 = f2 by A1, A2, A19, A21, A30;
A39: len (f1 ^ <*(upper_bound X)*>) = n + (len <*(upper_bound X)*>) by A19, FINSEQ_1:35
.= len v1 by A2, FINSEQ_1:56 ;
X: dom v1 = Seg (len v1) by FINSEQ_1:def 3;
now
let i be Nat; :: thesis: ( i in dom v1 implies (f1 ^ <*(upper_bound X)*>) . i = v1 . i )
assume i in dom v1 ; :: thesis: (f1 ^ <*(upper_bound X)*>) . i = v1 . i
then A40: ( 1 <= i & i <= (len f1) + 1 ) by A2, A19, X, FINSEQ_1:3;
now
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, A5, A7, A19, FINSEQ_1:59; :: thesis: verum
end;
suppose i <> (len f1) + 1 ; :: thesis: (f1 ^ <*(upper_bound X)*>) . i = v1 . i
then i < (len f1) + 1 by A40, XXREAL_0:1;
then i <= len f1 by NAT_1:13;
then A41: i in dom f1 by A18, A19, A40, FINSEQ_1:3;
hence (f1 ^ <*(upper_bound X)*>) . i = f1 . i by FINSEQ_1:def 7
.= v1 . i by A41, FUNCT_1:70 ;
:: thesis: verum
end;
end;
end;
hence (f1 ^ <*(upper_bound X)*>) . i = v1 . i ; :: thesis: verum
end;
then A42: v1 = f1 ^ <*(upper_bound X)*> by A39, FINSEQ_2:10;
A43: len (f2 ^ <*(upper_bound X)*>) = n + (len <*(upper_bound X)*>) by A19, FINSEQ_1:35
.= len v2 by A2, FINSEQ_1:56 ;
X: dom v2 = Seg (len v2) by FINSEQ_1:def 3;
now
let i be Nat; :: thesis: ( i in dom v2 implies (f2 ^ <*(upper_bound X)*>) . i = v2 . i )
assume i in dom v2 ; :: thesis: (f2 ^ <*(upper_bound X)*>) . i = v2 . i
then A44: ( 1 <= i & i <= (len f2) + 1 ) by A2, A19, X, FINSEQ_1:3;
now
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 A2, A11, A13, A19, FINSEQ_1:59; :: thesis: verum
end;
suppose i <> (len f2) + 1 ; :: thesis: (f2 ^ <*(upper_bound X)*>) . i = v2 . i
then i < (len f2) + 1 by A44, XXREAL_0:1;
then i <= len f2 by NAT_1:13;
then A45: i in dom f2 by A18, A19, A44, FINSEQ_1:3;
hence (f2 ^ <*(upper_bound X)*>) . i = f2 . i by FINSEQ_1:def 7
.= v2 . i by A45, FUNCT_1:70 ;
:: thesis: verum
end;
end;
end;
hence (f2 ^ <*(upper_bound X)*>) . i = v2 . i ; :: thesis: verum
end;
hence v1 = v2 by A38, A42, A43, FINSEQ_2:10; :: thesis: verum