theorem ZeZe: :: NDIFF_7:17

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