theorem ZeZe: :: LOPBAN12:3

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