theorem :: RLSUB_1:75

for V being RealLinearSpace holds the carrier of V is Coset of (Omega). V