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

A9: now :: thesis: for n being Nat holds (a #Q s) . n = ((a #Q sb) . n) * ((a #Q sc) . n)

let n be Nat; :: thesis: (a #Q s) . n = ((a #Q sb) . n) * ((a #Q sc) . n)
thus (a #Q s) . n = a #Q (s . n) by Def5
.= a #Q ((sb . n) + (sc . n)) by SEQ_1:7
.= (a #Q (sb . n)) * (a #Q (sc . n)) by A5, Th53
.= (a #Q (sb . n)) * ((a #Q sc) . n) by Def5
.= ((a #Q sb) . n) * ((a #Q sc) . n) by Def5 ; :: thesis: verum

end;

A10: s is convergent by A1, A3;
then a #Q s is convergent by A5, Th69;
hence a #R (b + c) = lim (a #Q s) by A5, A10, A8, Def6
.= lim ((a #Q sb) (#) (a #Q sc)) by A9, SEQ_1:8
.= (lim (a #Q sb)) * (lim (a #Q sc)) by A6, A7, SEQ_2:15
.= (a #R b) * (lim (a #Q sc)) by A5, A1, A2, A6, Def6
.= (a #R b) * (a #R c) by A5, A3, A4, A7, Def6 ;
:: thesis: verum