:: deftheorem defines (Omega). RUSUB_1:def 3 :
for V being RealUnitarySpace holds (Omega). V = UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #);