theorem Th18: :: LOPBAN15:16

for X being RealLinearSpace holds RLSp2RVSp ((0). X) = (0). (RLSp2RVSp X)