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

now

let n be Element of 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 Def7
.= (a #Q (s1 . n)) * (b #Q (s1 . n)) by A1, Th67
.= ((a #Q s1) . n) * (b #Q (s1 . n)) by Def7
.= ((a #Q s1) . n) * ((b #Q s1) . n) by Def7 ; :: thesis: verum

end;

then A6: (a * b) #Q s1 = (a #Q s1) (#) (b #Q s1) by SEQ_1:12;
then (a * b) #Q s1 is convergent by A4, A5, SEQ_2:28;
hence (a * b) #R c = lim ((a * b) #Q s1) by A2, A3, Def8
.= (lim (a #Q s1)) * (lim (b #Q s1)) by A4, A5, A6, SEQ_2:29
.= (a #R c) * (lim (b #Q s1)) by A1, A3, A4, Def8
.= (a #R c) * (b #R c) by A1, A3, A5, Def8 ;
:: thesis: verum