let V be RealUnitarySpace; :: thesis: for v being VECTOR of V holds v + ((Omega). V) = the carrier of V
let v be VECTOR of V; :: thesis: v + ((Omega). V) = the carrier of V
v in (Omega). V by STRUCT_0:def 5;
hence v + ((Omega). V) = the carrier of V by Lm3; :: thesis: verum