theorem :: RUSUB_3:3

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