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