theorem :: NORMSP_1:1

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