let a, b, c be real number ; :: 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 Element of NAT holds sb . n <= b by Th79;
consider sc being Rational_Sequence such that
A3: sc is convergent and
A4: c = lim sc and
for n being Element of NAT holds sc . n <= c by Th79;
assume A5: a > 0 ; :: thesis: a #R (b + c) = (a #R b) * (a #R c)
then A6: a #Q sb is convergent by A1, Th82;
A7: a #Q sc is convergent by A5, A3, Th82;
reconsider s = sb + sc as Rational_Sequence ;
A8: lim s = b + c by A1, A2, A3, A4, SEQ_2:20;

A9: now

let n be Element of NAT ; :: thesis: (a #Q s) . n = ((a #Q sb) . n) * ((a #Q sc) . n)
thus (a #Q s) . n = a #Q (s . n) by Def7
.= a #Q ((sb . n) + (sc . n)) by SEQ_1:11
.= (a #Q (sb . n)) * (a #Q (sc . n)) by A5, Th64
.= (a #Q (sb . n)) * ((a #Q sc) . n) by Def7
.= ((a #Q sb) . n) * ((a #Q sc) . n) by Def7 ; :: thesis: verum

end;

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