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

hence S is convergent by A1, A2, A3, Th8; :: thesis: verum

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

then
s is bounded_above
by SEQ_2:def 3;
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;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

hence S is convergent by A1, A2, A3, Th8; :: thesis: verum