let a, b, c be real number ; :: 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, XREAL_1:131;
consider s1 being Rational_Sequence such that
A4: s1 is convergent and
A5: c = lim s1 and
for n being Element of NAT holds s1 . n >= c by Th80;
A6: a #Q s1 is convergent by A1, A4, Th82;
A7: b #Q s1 is convergent by A2, A4, 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, A2, 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 A8: (a * b) #Q s1 = (a #Q s1) (#) (b #Q s1) by SEQ_1:12;
then (a * b) #Q s1 is convergent by A6, A7, SEQ_2:28;
hence (a * b) #R c = lim ((a * b) #Q s1) by A3, A4, A5, Def8
.= (lim (a #Q s1)) * (lim (b #Q s1)) by A6, A7, A8, SEQ_2:29
.= (a #R c) * (lim (b #Q s1)) by A1, A4, A5, A6, Def8
.= (a #R c) * (b #R c) by A2, A4, A5, A7, Def8 ;
:: thesis: verum