theorem Th2: :: RSSPACE2:2

for x, y, z being Point of l2_Space
for a being Real holds
( ( x .|. x = 0 implies x = 0. l2_Space ) & ( x = 0. l2_Space implies x .|. x = 0 ) & 0 <= x .|. x & x .|. y = y .|. x & (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) )