let S be RealUnitarySpace; :: thesis: for M being non empty Subset of S
for L being Subset of S st L = the carrier of (Ort_Comp M) holds
L is closed Subset of (TopSpaceNorm (RUSp2RNSp S))
let M be non empty Subset of S; :: thesis: for L being Subset of S st L = the carrier of (Ort_Comp M) holds
L is closed Subset of (TopSpaceNorm (RUSp2RNSp S))
let L be Subset of S; :: thesis: ( L = the carrier of (Ort_Comp M) implies L is closed Subset of (TopSpaceNorm (RUSp2RNSp S)) )
assume L = the carrier of (Ort_Comp M) ; :: thesis: L is closed Subset of (TopSpaceNorm (RUSp2RNSp S))
then for seq being sequence of S st rng seq c= L & seq is convergent holds
lim seq in L by Th21;
hence L is closed Subset of (TopSpaceNorm (RUSp2RNSp S)) by Th12; :: thesis: verum