for n being Element of NAT holds RN_Base n is Basis of REAL-US n