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 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) = lim (a #Q s) )
thus ex s being Rational_Sequence st
( s is convergent & lim s = b & a #Q s is convergent & lim (a #Q s) = lim (a #Q s) ) by A1, A2, A3, Th69; :: thesis: verum