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

a #R p = a #Q p

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

assume A1: a > 0 ; :: thesis: a #R p = a #Q p

set s = seq_const p;

A2: lim (seq_const p) = (seq_const p) . 0 by SEQ_4:26

.= p by FUNCOP_1:7 ;

reconsider s = seq_const p as Rational_Sequence ;

then A4: a #Q s is constant by A3, VALUED_0:def 18;

then lim (a #Q s) = (a #Q s) . 0 by SEQ_4:26

.= a #Q p by A3 ;

hence a #R p = a #Q p by A1, A2, A4, Def6; :: thesis: verum

a #R p = a #Q p

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

assume A1: a > 0 ; :: thesis: a #R p = a #Q p

set s = seq_const p;

A2: lim (seq_const p) = (seq_const p) . 0 by SEQ_4:26

.= p by FUNCOP_1:7 ;

reconsider s = seq_const p as Rational_Sequence ;

A3: now :: thesis: for n being Nat holds (a #Q s) . n = a #Q p

a #Q p in REAL
by XREAL_0:def 1;let n be Nat; :: thesis: (a #Q s) . n = a #Q p

reconsider nn = n as Element of NAT by ORDINAL1:def 12;

thus (a #Q s) . n = a #Q (s . nn) by Def5

.= a #Q p by FUNCOP_1:7 ; :: thesis: verum

end;reconsider nn = n as Element of NAT by ORDINAL1:def 12;

thus (a #Q s) . n = a #Q (s . nn) by Def5

.= a #Q p by FUNCOP_1:7 ; :: thesis: verum

then A4: a #Q s is constant by A3, VALUED_0:def 18;

then lim (a #Q s) = (a #Q s) . 0 by SEQ_4:26

.= a #Q p by A3 ;

hence a #R p = a #Q p by A1, A2, A4, Def6; :: thesis: verum