theorem defISOA2: :: NDIFF_7:19

for X, Y being RealNormSpace holds ((IsoCPNrSP (X,Y)) ") . (0. (product <*X,Y*>)) = 0. [:X,Y:]