set V = RealVectSpace (Seg n);
set T = TopSpaceMetr (EMINFTY n);
the topology of (TopSpaceMetr (EMINFTY n)) c= bool the carrier of (RealVectSpace (Seg n))

proof

let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in the topology of (TopSpaceMetr (EMINFTY n)) or t in bool the carrier of (RealVectSpace (Seg n)) )
assume t in the topology of (TopSpaceMetr (EMINFTY n)) ; :: thesis: t in bool the carrier of (RealVectSpace (Seg n))
then ( t in bool (REAL n) & REAL n = Funcs ((Seg n),REAL) ) by FINSEQ_2:93;
hence t in bool the carrier of (RealVectSpace (Seg n)) ; :: thesis: verum

end;

then reconsider t = the topology of (TopSpaceMetr (EMINFTY n)) as Subset-Family of the carrier of (RealVectSpace (Seg n)) ;
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 (EMINFTY 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 (EMINFTY 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