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