let a, b, c be real number ; :: 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 Element of NAT holds s . n <= c by Th79;
A3: lim (b (#) s) = b * c by A1, A2, SEQ_2:8;
A4: b (#) s is convergent by A1, SEQ_2:7;
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, Th82, Th95;

A7: 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 A5, Lm11
.= a #R ((b (#) s) . n) by SEQ_1:9 ; :: thesis: verum

end;

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