let n be non zero Nat; :: thesis: 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) #)
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) #) = RealVectSpace (Seg n) by EUCLID:def 8;
hence 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) #) by Def8; :: thesis: verum