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

A4: now

let n be Element of 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, Th63;
((a #Q s1) . n) #Q p = (a #Q (s1 . n)) #Q p by Def7
.= a #Q (p * (s1 . n)) by A3, Th70
.= a #Q (s2 . n) by SEQ_1:9
.= (a #Q s2) . n by Def7 ;
hence ( (a #Q s1) . n > 0 & ((a #Q s1) . n) #Q p = (a #Q s2) . n ) by A5, Def7; :: thesis: verum

end;

A6: s2 is convergent by A1, SEQ_2:7;
then A7: a #Q s2 is convergent by A3, Th82;
lim s2 = b * p by A1, A2, SEQ_2:8;
then A8: a #R (b * p) = lim (a #Q s2) by A3, A6, A7, Def8;
A9: a #Q s1 is convergent by A3, A1, Th82;
then a #R b = lim (a #Q s1) by A3, A1, A2, Def8;
hence (a #R b) #Q p = a #R (b * p) by A3, A9, A7, A8, A4, Th95, Th103; :: thesis: verum