set A = (len C) + 1;
defpred S2[ natural number , set ] means ( ( $1 = 1 implies $2 = r ) & ( $1 = (len C) + 1 implies $2 = s ) & ( 2 <= $1 & $1 <= len C implies $2 in ].(lower_bound (C /. $1)),(upper_bound (C /. ($1 - 1))).[ ) );
A5: 0 + 1 <= len C by A1, A2, A3, A4, Th65;
then A6: 0 + 1 < (len C) + 1 by XREAL_1:8;
A7: for k being Nat st k in Seg ((len C) + 1) holds
ex x being Element of REAL st S2[k,x]
proof
let k be Nat; :: thesis: ( k in Seg ((len C) + 1) implies ex x being Element of REAL st S2[k,x] )
assume k in Seg ((len C) + 1) ; :: thesis: ex x being Element of REAL st S2[k,x]
then A8: ( 1 <= k & k <= (len C) + 1 ) by FINSEQ_1:3;
reconsider r = r, s = s as Real by XREAL_0:def 1;
A9: (len C) + 0 < (len C) + 1 by XREAL_1:8;
per cases ( k = 1 or k = (len C) + 1 or ( 1 < k & k < (len C) + 1 ) ) by A8, XXREAL_0:1;
suppose A10: k = 1 ; :: thesis: ex x being Element of REAL st S2[k,x]
take r ; :: thesis: S2[k,r]
thus S2[k,r] by A5, A10; :: thesis: verum
end;
suppose A11: k = (len C) + 1 ; :: thesis: ex x being Element of REAL st S2[k,x]
take s ; :: thesis: S2[k,s]
thus S2[k,s] by A1, A2, A3, A4, A9, A11, Th65; :: thesis: verum
end;
suppose that A12: 1 < k and
A13: k < (len C) + 1 ; :: thesis: ex x being Element of REAL st S2[k,x]
k - 1 in NAT by A12, INT_1:18;
then A14: k - 1 is Nat ;
1 - 1 < k - 1 by A12, XREAL_1:16;
then A15: 0 + 1 <= k - 1 by A14, NAT_1:13;
k <= len C by A13, NAT_1:13;
then not ].(lower_bound (C /. ((k - 1) + 1))),(upper_bound (C /. (k - 1))).[ is empty by A1, A2, A3, A4, A14, A15, Th69;
then consider x being set such that
A16: x in ].(lower_bound (C /. ((k - 1) + 1))),(upper_bound (C /. (k - 1))).[ by XBOOLE_0:def 1;
reconsider x = x as Real by A16;
take x ; :: thesis: S2[k,x]
thus S2[k,x] by A12, A13, A16; :: thesis: verum
end;
end;
end;
consider p being FinSequence of REAL such that
A17: dom p = Seg ((len C) + 1) and
A18: for k being Nat st k in Seg ((len C) + 1) holds
S2[k,p . k] from FINSEQ_1:sch 5(A7);
 take p ; :: thesis: ( len p = (len C) + 1 & p . 1 = r & p . (len p) = s & ( for n being natural number st 1 <= n & n + 1 < len p holds
p . (n + 1) in ].(lower_bound (C /. (n + 1))),(upper_bound (C /. n)).[ ) )
thus A19: len p = (len C) + 1 by A17, FINSEQ_1:def 3; :: thesis: ( p . 1 = r & p . (len p) = s & ( for n being natural number st 1 <= n & n + 1 < len p holds
p . (n + 1) in ].(lower_bound (C /. (n + 1))),(upper_bound (C /. n)).[ ) )
1 in Seg ((len C) + 1) by A6, FINSEQ_1:3;
hence p . 1 = r by A18; :: thesis: ( p . (len p) = s & ( for n being natural number st 1 <= n & n + 1 < len p holds
p . (n + 1) in ].(lower_bound (C /. (n + 1))),(upper_bound (C /. n)).[ ) )
len p in Seg ((len C) + 1) by A6, A19, FINSEQ_1:3;
hence p . (len p) = s by A18, A19; :: thesis: for n being natural number st 1 <= n & n + 1 < len p holds
p . (n + 1) in ].(lower_bound (C /. (n + 1))),(upper_bound (C /. n)).[
let n be natural number ; :: thesis: ( 1 <= n & n + 1 < len p implies p . (n + 1) in ].(lower_bound (C /. (n + 1))),(upper_bound (C /. n)).[ )
assume A20: 1 <= n ; :: thesis: ( not n + 1 < len p or p . (n + 1) in ].(lower_bound (C /. (n + 1))),(upper_bound (C /. n)).[ )
assume A21: n + 1 < len p ; :: thesis: p . (n + 1) in ].(lower_bound (C /. (n + 1))),(upper_bound (C /. n)).[
then A22: n + 1 <= len C by A19, NAT_1:13;
0 + 1 <= n + 1 by XREAL_1:8;
then A23: n + 1 in Seg ((len C) + 1) by A19, A21, FINSEQ_1:3;
1 + 1 <= n + 1 by A20, XREAL_1:8;
then p . (n + 1) in ].(lower_bound (C /. (n + 1))),(upper_bound (C /. ((n + 1) - 1))).[ by A18, A22, A23;
hence p . (n + 1) in ].(lower_bound (C /. (n + 1))),(upper_bound (C /. n)).[ ; :: thesis: verum