let a be real number ; :: thesis: ( a > 0 implies a #R 1 = a )
assume A1: a > 0 ; :: thesis: a #R 1 = a
reconsider s = NAT --> 1 as Real_Sequence by FUNCOP_1:57;
for n being Element of NAT holds s . n is Rational ;
then reconsider s = s as Rational_Sequence by Def6;
s . 0 = 1 by FUNCOP_1:13;
then A3: lim s = 1 by SEQ_4:41;
Y: a in REAL by XREAL_0:def 1;

A4: now

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

end;

then A5: a #Q s is constant by Y, VALUED_0:def 18;
then A6: a #Q s is convergent ;
(a #Q s) . 0 = a by A4;
then lim (a #Q s) = a by A5, SEQ_4:41;
hence a #R 1 = a by A1, A3, A6, Def8; :: thesis: verum