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;

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

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)

then A8:
(a * b) #Q s1 = (a #Q s1) (#) (b #Q s1)
by SEQ_1:8;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;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

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