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 convergent holds

( S is convergent & lim s = lim S )

let s be Real_Sequence; :: thesis: for S being sequence of (Closed-Interval-MSpace (a,b)) st S = s & a <= b & s is convergent holds

( S is convergent & lim s = lim S )

let S be sequence of (Closed-Interval-MSpace (a,b)); :: thesis: ( S = s & a <= b & s is convergent implies ( S is convergent & lim s = lim S ) )

assume that

A1: S = s and

A2: a <= b and

A3: s is convergent ; :: thesis: ( S is convergent & lim s = lim S )

reconsider S0 = S as sequence of RealSpace by A2, Th6;

A4: S0 is convergent by A1, A3, Th4;

hence S is convergent by A2, Th7; :: thesis: lim s = lim S

lim S0 = lim S by A2, A4, Th7;

hence lim s = lim S by A1, A3, Th4; :: thesis: verum

for S being sequence of (Closed-Interval-MSpace (a,b)) st S = s & a <= b & s is convergent holds

( S is convergent & lim s = lim S )

let s be Real_Sequence; :: thesis: for S being sequence of (Closed-Interval-MSpace (a,b)) st S = s & a <= b & s is convergent holds

( S is convergent & lim s = lim S )

let S be sequence of (Closed-Interval-MSpace (a,b)); :: thesis: ( S = s & a <= b & s is convergent implies ( S is convergent & lim s = lim S ) )

assume that

A1: S = s and

A2: a <= b and

A3: s is convergent ; :: thesis: ( S is convergent & lim s = lim S )

reconsider S0 = S as sequence of RealSpace by A2, Th6;

A4: S0 is convergent by A1, A3, Th4;

hence S is convergent by A2, Th7; :: thesis: lim s = lim S

lim S0 = lim S by A2, A4, Th7;

hence lim s = lim S by A1, A3, Th4; :: thesis: verum