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:93;
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:93; :: 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