TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by Def8;
hence TOP-REAL n is TopSpace-like by PRE_TOPC:28; :: thesis: ( TOP-REAL n is Abelian & TOP-REAL n is add-associative & TOP-REAL n is right_zeroed & TOP-REAL n is right_complementable & TOP-REAL n is vector-distributive & TOP-REAL n is scalar-distributive & TOP-REAL n is scalar-associative & TOP-REAL n is scalar-unital )
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 Def8;
hence ( TOP-REAL n is Abelian & TOP-REAL n is add-associative & TOP-REAL n is right_zeroed & TOP-REAL n is right_complementable & TOP-REAL n is vector-distributive & TOP-REAL n is scalar-distributive & TOP-REAL n is scalar-associative & TOP-REAL n is scalar-unital ) by RSSPACE:15; :: thesis: verum