for RNS being RealNormSpace holds ||.(0. RNS).|| = 0 ;