for F being Field
for V, W being VectSp of F st (Omega). W is Subspace of V holds
W is Subspace of V