theorem :: RUSUB_5:22

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