theorem LMQ20: :: NORMSP_3:63

for V being RealLinearSpace
for W being Subspace of V ex QL being LinearOperator of V,(VectQuot (V,W)) st
( QL is onto & ( for v being VECTOR of V holds QL . v = v + W ) )