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;

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

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;

then j #Q s is constant by VALUED_0:def 18;
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