let a be real number ; :: thesis: for p being Rational st a > 0 holds
a #R p = a #Q p
let p be Rational; :: thesis: ( a > 0 implies a #R p = a #Q p )
assume A1: a > 0 ; :: thesis: a #R p = a #Q p
p in REAL by XREAL_0:def 1;
then reconsider s = NAT --> p as Real_Sequence by FUNCOP_1:57;
A3: lim s = s . 0 by SEQ_4:41
.= p by FUNCOP_1:13 ;
for n being Element of NAT holds s . n is Rational ;
then reconsider s = s as Rational_Sequence by Def6;
Y: a #Q p in REAL by XREAL_0:def 1;

A4: now

let n be Nat; :: thesis: (a #Q s) . n = a #Q p
reconsider nn = n as Element of NAT by ORDINAL1:def 13;
thus (a #Q s) . n = a #Q (s . nn) by Def7
.= a #Q p by FUNCOP_1:13 ; :: thesis: verum

end;

then A5: a #Q s is constant by Y, VALUED_0:def 18;
then A6: a #Q s is convergent ;
lim (a #Q s) = (a #Q s) . 0 by A5, SEQ_4:41
.= a #Q p by A4 ;
hence a #R p = a #Q p by A1, A3, A6, Def8; :: thesis: verum