let a be Real; :: thesis: 1 #R a = 1

consider s being Rational_Sequence such that

A1: s is convergent and

A2: a = lim s and

for n being Nat holds s . n <= a by Th67;

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

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

.= 1 by A3 ;

1 #Q s is convergent by A1, Th69;

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

consider s being Rational_Sequence such that

A1: s is convergent and

A2: a = lim s and

for n being Nat holds s . n <= a by Th67;

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

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

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

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

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

.= j by Th51 ; :: thesis: verum

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

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

.= j by Th51 ; :: thesis: verum

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

.= 1 by A3 ;

1 #Q s is convergent by A1, Th69;

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