let a, b, c be Real; :: thesis: ( a > 0 implies (a #R b) #R c = a #R (b * c) )
consider s being Rational_Sequence such that
A1: s is convergent and
A2: c = lim s and
for n being Nat holds s . n <= c by Th67;
A3: lim (b (#) s) = b * c by A1, A2, SEQ_2:8;
A4: b (#) s is convergent by A1;
assume A5: a > 0 ; :: thesis: (a #R b) #R c = a #R (b * c)
then A6: (a #R b) #Q s is convergent by A1, Th69, Th81;

A7: now :: thesis: for n being Nat holds ((a #R b) #Q s) . n = a #R ((b (#) s) . n)

let n be Nat; :: thesis: ((a #R b) #Q s) . n = a #R ((b (#) s) . n)
thus ((a #R b) #Q s) . n = (a #R b) #Q (s . n) by Def5
.= a #R (b * (s . n)) by A5, Lm11
.= a #R ((b (#) s) . n) by SEQ_1:9 ; :: thesis: verum

end;

a #R b > 0 by A5, Th81;
then (a #R b) #R c = lim ((a #R b) #Q s) by A1, A2, A6, Def6;
hence (a #R b) #R c = a #R (b * c) by A5, A6, A4, A3, A7, Th90; :: thesis: verum