theorem :: LOPBAN14:3

for X being RealLinearSpace holds ((IsoCPRLSP X) ") . (0. (product <*X*>)) = 0. X