let a be real number ; :: 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 Element of NAT holds s . n <= a by Th79;

A3: now

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

end;

then 1 #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, Th82;
hence 1 #R a = 1 by A1, A2, A4, Def8; :: thesis: verum