let a, b, c be real number ; :: thesis: ( a > 0 implies a #R (b + c) = (a #R b) * (a #R c) )
assume A1: a > 0 ; :: thesis: a #R (b + c) = (a #R b) * (a #R c)
consider sb being Rational_Sequence such that
A2: ( sb is convergent & b = lim sb & ( for n being Element of NAT holds sb . n <= b ) ) by Th79;
A3: a #Q sb is convergent by A1, A2, Th82;
consider sc being Rational_Sequence such that
A4: ( sc is convergent & c = lim sc & ( for n being Element of NAT holds sc . n <= c ) ) by Th79;
A5: a #Q sc is convergent by A1, A4, Th82;

now

let n be Element of NAT ; :: thesis: (sb + sc) . n is Rational
(sb . n) + (sc . n) = (sb + sc) . n by SEQ_1:11;
hence (sb + sc) . n is Rational ; :: thesis: verum

end;

then reconsider s = sb + sc as Rational_Sequence by Def6;
A6: s is convergent by A2, A4, SEQ_2:19;
A7: lim s = b + c by A2, A4, SEQ_2:20;
A8: a #Q s is convergent by A1, A6, Th82;

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 A1, Th64
.= (a #Q (sb . n)) * ((a #Q sc) . n) by Def7
.= ((a #Q sb) . n) * ((a #Q sc) . n) by Def7 ; :: thesis: verum

end;

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