let a, b be Real; :: thesis: for p being Rational st a > 0 holds

(a #R b) #Q p = a #R (b * p)

let p be Rational; :: thesis: ( a > 0 implies (a #R b) #Q p = a #R (b * p) )

consider s1 being Rational_Sequence such that

A1: s1 is convergent and

A2: b = lim s1 and

for n being Nat holds s1 . n >= b by Th68;

reconsider s2 = p (#) s1 as Rational_Sequence ;

assume A3: a > 0 ; :: thesis: (a #R b) #Q p = a #R (b * p)

then A7: a #Q s2 is convergent by A3, Th69;

lim s2 = b * p by A1, A2, SEQ_2:8;

then A8: a #R (b * p) = lim (a #Q s2) by A3, A6, A7, Def6;

A9: a #Q s1 is convergent by A3, A1, Th69;

then a #R b = lim (a #Q s1) by A3, A1, A2, Def6;

hence (a #R b) #Q p = a #R (b * p) by A3, A9, A7, A8, A4, Th81, Th89; :: thesis: verum

(a #R b) #Q p = a #R (b * p)

let p be Rational; :: thesis: ( a > 0 implies (a #R b) #Q p = a #R (b * p) )

consider s1 being Rational_Sequence such that

A1: s1 is convergent and

A2: b = lim s1 and

for n being Nat holds s1 . n >= b by Th68;

reconsider s2 = p (#) s1 as Rational_Sequence ;

assume A3: a > 0 ; :: thesis: (a #R b) #Q p = a #R (b * p)

A4: now :: thesis: for n being Nat holds

( (a #Q s1) . n > 0 & ((a #Q s1) . n) #Q p = (a #Q s2) . n )

A6:
s2 is convergent
by A1;( (a #Q s1) . n > 0 & ((a #Q s1) . n) #Q p = (a #Q s2) . n )

let n be Nat; :: thesis: ( (a #Q s1) . n > 0 & ((a #Q s1) . n) #Q p = (a #Q s2) . n )

A5: a #Q (s1 . n) > 0 by A3, Th52;

((a #Q s1) . n) #Q p = (a #Q (s1 . n)) #Q p by Def5

.= a #Q (p * (s1 . n)) by A3, Th59

.= a #Q (s2 . n) by SEQ_1:9

.= (a #Q s2) . n by Def5 ;

hence ( (a #Q s1) . n > 0 & ((a #Q s1) . n) #Q p = (a #Q s2) . n ) by A5, Def5; :: thesis: verum

end;A5: a #Q (s1 . n) > 0 by A3, Th52;

((a #Q s1) . n) #Q p = (a #Q (s1 . n)) #Q p by Def5

.= a #Q (p * (s1 . n)) by A3, Th59

.= a #Q (s2 . n) by SEQ_1:9

.= (a #Q s2) . n by Def5 ;

hence ( (a #Q s1) . n > 0 & ((a #Q s1) . n) #Q p = (a #Q s2) . n ) by A5, Def5; :: thesis: verum

then A7: a #Q s2 is convergent by A3, Th69;

lim s2 = b * p by A1, A2, SEQ_2:8;

then A8: a #R (b * p) = lim (a #Q s2) by A3, A6, A7, Def6;

A9: a #Q s1 is convergent by A3, A1, Th69;

then a #R b = lim (a #Q s1) by A3, A1, A2, Def6;

hence (a #R b) #Q p = a #R (b * p) by A3, A9, A7, A8, A4, Th81, Th89; :: thesis: verum