let a, b be Real; :: thesis: for s being Real_Sequence
for S being sequence of (Closed-Interval-MSpace (a,b)) st S = s & a <= b & s is non-decreasing holds
S is convergent
let s be Real_Sequence; :: thesis: for S being sequence of (Closed-Interval-MSpace (a,b)) st S = s & a <= b & s is non-decreasing holds
S is convergent
let S be sequence of (Closed-Interval-MSpace (a,b)); :: thesis: ( S = s & a <= b & s is non-decreasing implies S is convergent )
assume that
A1: S = s and
A2: a <= b and
A3: s is non-decreasing ; :: thesis: S is convergent
for n being Nat holds s . n < b + 1
proof
let n be Nat; :: thesis: s . n < b + 1
A4: b < b + 1 by XREAL_1:29;
A5: n in NAT by ORDINAL1:def 12;
dom S = NAT by FUNCT_2:def 1;
then A6: s . n in rng S by A1, FUNCT_1:def 3, A5;
the carrier of (Closed-Interval-MSpace (a,b)) = [.a,b.] by A2, TOPMETR:10;
then s . n <= b by A6, XXREAL_1:1;
hence s . n < b + 1 by A4, XXREAL_0:2; :: thesis: verum
end;
then s is bounded_above by SEQ_2:def 3;
hence S is convergent by A1, A2, A3, Th8; :: thesis: verum