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