let a be Real; :: thesis: ( a > 0 implies a #R 0 = 1 )

set s = seq_const 0;

reconsider s = seq_const 0 as Rational_Sequence ;

assume A1: a > 0 ; :: thesis: a #R 0 = 1

s . 0 = 0 ;

then A2: lim s = 0 by SEQ_4:26;

reconsider j = 1 as Element of REAL by NUMBERS:19;

(a #Q s) . 0 = 1 by A3;

then lim (a #Q s) = 1 by A4, SEQ_4:26;

hence a #R 0 = 1 by A1, A2, A4, Def6; :: thesis: verum

set s = seq_const 0;

reconsider s = seq_const 0 as Rational_Sequence ;

assume A1: a > 0 ; :: thesis: a #R 0 = 1

s . 0 = 0 ;

then A2: lim s = 0 by SEQ_4:26;

reconsider j = 1 as Element of REAL by NUMBERS:19;

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

then A4:
a #Q s is constant
by VALUED_0:def 18;let n be Nat; :: thesis: (a #Q s) . n = j

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

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

.= j by Th47 ; :: 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

.= j by Th47 ; :: thesis: verum

(a #Q s) . 0 = 1 by A3;

then lim (a #Q s) = 1 by A4, SEQ_4:26;

hence a #R 0 = 1 by A1, A2, A4, Def6; :: thesis: verum