consider s being Rational_Sequence such that

A2: s is convergent and

A3: lim s = b and

for n being Nat holds s . n <= b by Th67;

take IT = lim (a #Q s); :: thesis: ex s being Rational_Sequence st

( s is convergent & lim s = b & a #Q s is convergent & lim (a #Q s) = IT )

thus ex s being Rational_Sequence st

( s is convergent & lim s = b & a #Q s is convergent & lim (a #Q s) = IT ) by A1, A2, A3, Th69; :: thesis: verum

A2: s is convergent and

A3: lim s = b and

for n being Nat holds s . n <= b by Th67;

take IT = lim (a #Q s); :: thesis: ex s being Rational_Sequence st

( s is convergent & lim s = b & a #Q s is convergent & lim (a #Q s) = IT )

thus ex s being Rational_Sequence st

( s is convergent & lim s = b & a #Q s is convergent & lim (a #Q s) = IT ) by A1, A2, A3, Th69; :: thesis: verum