:: deftheorem Def6 defines #R PREPOWER:def 7 :
for a, b being Real st a > 0 holds
for b₃ being Real holds
( b₃ = a #R b iff ex s being Rational_Sequence st
( s is convergent & lim s = b & a #Q s is convergent & lim (a #Q s) = b₃ ) );