let n be Nat; :: thesis: 0. (TOP-REAL n) = 0. (REAL-NS n)
thus 0. (TOP-REAL n) = 0. 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) #)
.= 0. 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
.= 0. (REAL-NS n) ; :: thesis: verum