let a, b be Real; :: 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) )
consider s1 being Rational_Sequence such that
A1: s1 is convergent and
A2: b = lim s1 and
for n being Nat holds s1 . n >= b by Th68;
reconsider s2 = p (#) s1 as Rational_Sequence ;
assume A3: a > 0 ; :: thesis: (a #R b) #Q p = a #R (b * p)

A4: now :: thesis: for n being Nat holds
( (a #Q s1) . n > 0 & ((a #Q s1) . n) #Q p = (a #Q s2) . n )

let n be Nat; :: thesis: ( (a #Q s1) . n > 0 & ((a #Q s1) . n) #Q p = (a #Q s2) . n )
A5: a #Q (s1 . n) > 0 by A3, Th52;
((a #Q s1) . n) #Q p = (a #Q (s1 . n)) #Q p by Def5
.= a #Q (p * (s1 . n)) by A3, Th59
.= a #Q (s2 . n) by SEQ_1:9
.= (a #Q s2) . n by Def5 ;
hence ( (a #Q s1) . n > 0 & ((a #Q s1) . n) #Q p = (a #Q s2) . n ) by A5, Def5; :: thesis: verum

end;

A6: s2 is convergent by A1;
then A7: a #Q s2 is convergent by A3, Th69;
lim s2 = b * p by A1, A2, SEQ_2:8;
then A8: a #R (b * p) = lim (a #Q s2) by A3, A6, A7, Def6;
A9: a #Q s1 is convergent by A3, A1, Th69;
then a #R b = lim (a #Q s1) by A3, A1, A2, Def6;
hence (a #R b) #Q p = a #R (b * p) by A3, A9, A7, A8, A4, Th81, Th89; :: thesis: verum