theorem LMQ05: :: NORMSP_3:54

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