let a be real number ; :: thesis: 1 #R a = 1
consider s being Rational_Sequence such that
A1: ( s is convergent & a = lim s & ( for n being Element of NAT holds s . n <= a ) ) by Th79;
A2: 1 #Q s is convergent by A1, Th82;

A3: now

let n be Nat; :: thesis: (1 #Q s) . n = 1
reconsider nn = n as Element of NAT by ORDINAL1:def 13;
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 lim (1 #Q s) = (1 #Q s) . 0 by SEQ_4:41
.= 1 by A3 ;
hence 1 #R a = 1 by A1, A2, Def8; :: thesis: verum