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

set s = seq_const 1;

reconsider s = seq_const 1 as Rational_Sequence ;

s . 0 = 1 by SEQ_1:57;

then A1: lim s = 1 by SEQ_4:26;

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

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

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

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

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

set s = seq_const 1;

reconsider s = seq_const 1 as Rational_Sequence ;

s . 0 = 1 by SEQ_1:57;

then A1: lim s = 1 by SEQ_4:26;

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

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

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

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

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

.= a by A2, Th48, SEQ_1:57 ; :: 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 by A2, Th48, SEQ_1:57 ; :: thesis: verum

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

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

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

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