let n be Nat; :: thesis: the carrier of (TOP-REAL n) = the carrier of (REAL-NS n)
thus the carrier of (TOP-REAL n) = the carrier of 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) #)
.= the carrier of RLSStruct(# the carrier of (REAL-NS n), the ZeroF of (REAL-NS n), the addF of (REAL-NS n), the Mult of (REAL-NS n) #) by Th1
.= the carrier of (REAL-NS n) ; :: thesis: verum