theorem :: LOPBAN14:12

for X being RealNormSpace holds 0. (product <*X*>) = (IsoCPNrSP X) . (0. X)