:: deftheorem defQuotR defines InducedBi NORMSP_3:def 16 :
for V, W being RealLinearSpace
for L being LinearOperator of V,W
for b₄ being LinearOperator of (VectQuot (V,(Ker L))),(Im L) holds
( b₄ = InducedBi (V,W,L) iff ( b₄ is isomorphism & ( for z being Point of (VectQuot (V,(Ker L)))
for v being VECTOR of V st z = v + (Ker L) holds
b₄ . z = L . v ) ) );