theorem :: NORMSP_3:65
for V, W being RealLinearSpace
for L being LinearOperator of V,W holds L = (InducedBi (V,W,L)) * (InducedSur (V,(Ker L)))