:: deftheorem defQuotN defines NVectQuot NORMSP_3:def 19 :
for X being RealNormSpace
for Y being Subspace of X st ex CY being Subset of X st
( CY = the carrier of Y & CY is closed ) holds
for b₃ being strict RealNormSpace holds
( b₃ = NVectQuot (X,Y) iff ( RLSStruct(# the carrier of b₃, the ZeroF of b₃, the addF of b₃, the Mult of b₃ #) = VectQuot (X,Y) & the normF of b₃ = NormCoset (X,Y) ) );