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;

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

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)

a #R b > 0
by A5, Th81;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;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

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