for V being RealUnitarySpace holds Lin ({} the carrier of V) = (0). V