let V, W be RealLinearSpace; :: thesis: for L being LinearOperator of V,W holds L = (InducedBi (V,W,L)) * (InducedSur (V,(Ker L)))
let L be LinearOperator of V,W; :: thesis: L = (InducedBi (V,W,L)) * (InducedSur (V,(Ker L)))

now :: thesis: for v being VECTOR of V holds ((InducedBi (V,W,L)) * (InducedSur (V,(Ker L)))) . v = L . v

let v be VECTOR of V; :: thesis: ((InducedBi (V,W,L)) * (InducedSur (V,(Ker L)))) . v = L . v
A1: dom (InducedSur (V,(Ker L))) = the carrier of V by FUNCT_2:def 1;
reconsider z = v + (Ker L) as Point of (VectQuot (V,(Ker L))) by LMQ07;
thus ((InducedBi (V,W,L)) * (InducedSur (V,(Ker L)))) . v = (InducedBi (V,W,L)) . ((InducedSur (V,(Ker L))) . v) by A1, FUNCT_1:13
.= (InducedBi (V,W,L)) . z by defDQuot
.= L . v by defQuotR ; :: thesis: verum

end;

hence L = (InducedBi (V,W,L)) * (InducedSur (V,(Ker L))) ; :: thesis: verum