for X being RealLinearSpace
for Y being Subspace of X holds CosetSet (X,Y) = CosetSet ((RLSp2RVSp X),(RLSp2RVSp Y))