theorem :: RUSUB_7:14

for S being RealUnitarySpace holds TopSpaceNorm (RUSp2RNSp S) = TopUnitSpace S