:: deftheorem defines VectQuot NORMSP_3:def 12 :
for X being RealLinearSpace
for Y being Subspace of X holds VectQuot (X,Y) = RVSp2RLSp (VectQuot ((RLSp2RVSp X),(RLSp2RVSp Y)));