let a, b, c be real number ; :: thesis: ( a > 0 implies (a #R b) #R c = a #R (b * c) )
assume A1: a > 0 ; :: thesis: (a #R b) #R c = a #R (b * c)
then A2: a #R b > 0 by Th95;
consider s being Rational_Sequence such that
A3: ( s is convergent & c = lim s & ( for n being Element of NAT holds s . n <= c ) ) by Th79;
A4: (a #R b) #Q s is convergent by A2, A3, Th82;
then A5: (a #R b) #R c = lim ((a #R b) #Q s) by A2, A3, Def8;
A6: b (#) s is convergent by A3, SEQ_2:21;
A7: lim (b (#) s) = b * c by A3, SEQ_2:22;

now

let n be Element of 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 Def7
.= a #R (b * (s . n)) by A1, Lm10
.= a #R ((b (#) s) . n) by SEQ_1:13 ; :: thesis: verum

end;

hence (a #R b) #R c = a #R (b * c) by A1, A4, A5, A6, A7, Th104; :: thesis: verum