set V = RealVectSpace (Seg n);
set T = TopSpaceMetr (Euclid n);
reconsider t = the topology of (TopSpaceMetr (Euclid n)) as Subset-Family of the carrier of (RealVectSpace (Seg n)) by FINSEQ_2:111;
take S = RLTopStruct(# the carrier of (RealVectSpace (Seg n)),the ZeroF of (RealVectSpace (Seg n)),the addF of (RealVectSpace (Seg n)),the Mult of (RealVectSpace (Seg n)),t #); :: thesis: ( TopStruct(# the carrier of S,the topology of S #) = TopSpaceMetr (Euclid n) & RLSStruct(# the carrier of S,the ZeroF of S,the addF of S,the Mult of S #) = RealVectSpace (Seg n) )
thus TopStruct(# the carrier of S,the topology of S #) = TopSpaceMetr (Euclid n) by FINSEQ_2:111; :: thesis: RLSStruct(# the carrier of S,the ZeroF of S,the addF of S,the Mult of S #) = RealVectSpace (Seg n)
thus RLSStruct(# the carrier of S,the ZeroF of S,the addF of S,the Mult of S #) = RealVectSpace (Seg n) ; :: thesis: verum