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)))

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

hence
L = (InducedBi (V,W,L)) * (InducedSur (V,(Ker L)))
; :: thesis: verumlet 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;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