theorem Th2: :: LOPBAN14:1

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