let a, b, c be Real; :: thesis: ( a > 0 & b > 0 implies (a * b) #R c = (a #R c) * (b #R c) )
assume that
A1: a > 0 and
A2: b > 0 ; :: thesis: (a * b) #R c = (a #R c) * (b #R c)
A3: a * b > 0 by A1, A2;
consider s1 being Rational_Sequence such that
A4: s1 is convergent and
A5: c = lim s1 and
for n being Nat holds s1 . n >= c by Th68;
A6: a #Q s1 is convergent by A1, A4, Th69;
A7: b #Q s1 is convergent by A2, A4, Th69;

now :: thesis: for n being Nat holds ((a * b) #Q s1) . n = ((a #Q s1) . n) * ((b #Q s1) . n)

let n be Nat; :: thesis: ((a * b) #Q s1) . n = ((a #Q s1) . n) * ((b #Q s1) . n)
thus ((a * b) #Q s1) . n = (a * b) #Q (s1 . n) by Def5
.= (a #Q (s1 . n)) * (b #Q (s1 . n)) by A1, A2, Th56
.= ((a #Q s1) . n) * (b #Q (s1 . n)) by Def5
.= ((a #Q s1) . n) * ((b #Q s1) . n) by Def5 ; :: thesis: verum

end;

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