theorem :: SRINGS_5:102

for n being non zero Nat holds RLSStruct(# the carrier of (TOP-REAL n), the ZeroF of (TOP-REAL n), the addF of (TOP-REAL n), the Mult of (TOP-REAL n) #) = RLSStruct(# the carrier of (TOP-REAL-INFTY n), the ZeroF of (TOP-REAL-INFTY n), the addF of (TOP-REAL-INFTY n), the Mult of (TOP-REAL-INFTY n) #)