for x being object
for V being RealLinearSpace holds
( x in (0). V iff x = 0. V ) by Lm2;