theorem Th3: :: MAZURULM:3

for E being RealNormSpace
for a being Point of E holds a + a = 2 * a