:: deftheorem defDQuot defines InducedSur NORMSP_3:def 15 :
for V being RealLinearSpace
for W being Subspace of V
for b₃ being LinearOperator of V,(VectQuot (V,W)) holds
( b₃ = InducedSur (V,W) iff ( b₃ is onto & ( for v being VECTOR of V holds b₃ . v = v + W ) ) );