let a be real number ; :: thesis: ( a > 0 implies a #R 0 = 1 )
reconsider s = NAT --> 0 as Real_Sequence by FUNCOP_1:45;
reconsider s = s as Rational_Sequence ;
assume A1: a > 0 ; :: thesis: a #R 0 = 1
s . 0 = 0 by FUNCOP_1:7;
then A2: lim s = 0 by SEQ_4:26;

A3: now

let n be Nat; :: thesis: (a #Q s) . n = 1
reconsider nn = n as Element of NAT by ORDINAL1:def 12;
thus (a #Q s) . n = a #Q (s . nn) by Def7
.= 1 by Th58, FUNCOP_1:7 ; :: thesis: verum

end;

then A4: a #Q s is constant by VALUED_0:def 18;
(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, Def8; :: thesis: verum