let V, W be RealLinearSpace; for L being LinearOperator of V,W holds L = (InducedBi (V,W,L)) * (InducedSur (V,(Ker L)))
let L be LinearOperator of V,W; L = (InducedBi (V,W,L)) * (InducedSur (V,(Ker L)))
now for v being VECTOR of V holds ((InducedBi (V,W,L)) * (InducedSur (V,(Ker L)))) . v = L . vlet v be
VECTOR of
V;
((InducedBi (V,W,L)) * (InducedSur (V,(Ker L)))) . v = L . vA1:
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
;
verum end;
hence
L = (InducedBi (V,W,L)) * (InducedSur (V,(Ker L)))
; verum