for V, W being RealLinearSpace
for L being LinearOperator of V,W ex QL being LinearOperator of (VectQuot (V,(Ker L))),(Im L) st
( QL is isomorphism & ( for z being Point of (VectQuot (V,(Ker L)))
for v being VECTOR of V st z = v + (Ker L) holds
QL . z = L . v ) )