let a, b, c be Real; ( a > 0 & b > 0 implies (a * b) #R c = (a #R c) * (b #R c) )
assume that
A1:
a > 0
and
A2:
b > 0
; (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;
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
;
verum