theorem :: RUSUB_5:23

for V being RealUnitarySpace holds Ort_Comp ((Omega). V) = (0). V