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;

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

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)

A10:
s is convergent
by A1, A3;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;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

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