let a, b be real number ; :: thesis: for p being Rational st a > 0 holds
(a #R b) #Q p = a #R (b * p)
let p be Rational; :: thesis: ( a > 0 implies (a #R b) #Q p = a #R (b * p) )
assume A1: a > 0 ; :: thesis: (a #R b) #Q p = a #R (b * p)
consider s1 being Rational_Sequence such that
A2: ( s1 is convergent & b = lim s1 & ( for n being Element of NAT holds s1 . n >= b ) ) by Th80;
A3: a #Q s1 is convergent by A1, A2, Th82;
then A4: a #R b = lim (a #Q s1) by A1, A2, Def8;
then A5: lim (a #Q s1) > 0 by A1, Th95;

now

let n be Element of NAT ; :: thesis: (p (#) s1) . n is Rational
(p (#) s1) . n = p * (s1 . n) by SEQ_1:13;
hence (p (#) s1) . n is Rational ; :: thesis: verum

end;

then reconsider s2 = p (#) s1 as Rational_Sequence by Def6;
A6: s2 is convergent by A2, SEQ_2:21;
then A7: a #Q s2 is convergent by A1, Th82;
lim s2 = b * p by A2, SEQ_2:22;
then A8: a #R (b * p) = lim (a #Q s2) by A1, A6, A7, Def8;

now

let n be Element of NAT ; :: thesis: ( (a #Q s1) . n > 0 & ((a #Q s1) . n) #Q p = (a #Q s2) . n )
A9: ((a #Q s1) . n) #Q p = (a #Q (s1 . n)) #Q p by Def7
.= a #Q (p * (s1 . n)) by A1, Th70
.= a #Q (s2 . n) by SEQ_1:13
.= (a #Q s2) . n by Def7 ;
a #Q (s1 . n) > 0 by A1, Th63;
hence ( (a #Q s1) . n > 0 & ((a #Q s1) . n) #Q p = (a #Q s2) . n ) by A9, Def7; :: thesis: verum

end;

hence (a #R b) #Q p = a #R (b * p) by A3, A4, A5, A7, A8, Th103; :: thesis: verum