let R be Ring; :: thesis: for V being LeftMod of R
for W being Subspace of V holds ker (ZQMorph (V,W)) = (Omega). W
let V be LeftMod of R; :: thesis: for W being Subspace of V holds ker (ZQMorph (V,W)) = (Omega). W
let W be Subspace of V; :: thesis: ker (ZQMorph (V,W)) = (Omega). W
set f = ZQMorph (V,W);
reconsider Ws = (Omega). W as strict Subspace of V by VECTSP_4:26;
for x being object holds
( x in (ZQMorph (V,W)) " {(0. (VectQuot (V,W)))} iff x in the carrier of W )

proof

let x be object ; :: thesis: ( x in (ZQMorph (V,W)) " {(0. (VectQuot (V,W)))} iff x in the carrier of W )

hereby :: thesis: ( x in the carrier of W implies x in (ZQMorph (V,W)) " {(0. (VectQuot (V,W)))} )

assume A11: x in (ZQMorph (V,W)) " {(0. (VectQuot (V,W)))} ; :: thesis: x in the carrier of W
then A1: ( x in the carrier of V & (ZQMorph (V,W)) . x in {(0. (VectQuot (V,W)))} ) by FUNCT_2:38;
reconsider v = x as Vector of V by A11;
(ZQMorph (V,W)) . v = 0. (VectQuot (V,W)) by A1, TARSKI:def 1
.= zeroCoset (V,W) by VECTSP10:def 6
.= the carrier of W ;
then v + W = the carrier of W by defMophVW;
then v in W by VECTSP_4:49;
hence x in the carrier of W ; :: thesis: verum

end;

assume B1: x in the carrier of W ; :: thesis: x in (ZQMorph (V,W)) " {(0. (VectQuot (V,W)))}
B4: the carrier of W c= the carrier of V by VECTSP_4:def 2;
then reconsider v = x as Vector of V by B1;
B2: v in W by B1;
(ZQMorph (V,W)) . v = v + W by defMophVW
.= zeroCoset (V,W) by B2, VECTSP_4:49
.= 0. (VectQuot (V,W)) by VECTSP10:def 6 ;
then (ZQMorph (V,W)) . x in {(0. (VectQuot (V,W)))} by TARSKI:def 1;
hence x in (ZQMorph (V,W)) " {(0. (VectQuot (V,W)))} by B1, B4, FUNCT_2:38; :: thesis: verum

end;

then (ZQMorph (V,W)) " {(0. (VectQuot (V,W)))} = the carrier of W by TARSKI:2;
then ker (ZQMorph (V,W)) = Ws by LMFirst2, VECTSP_4:29;
hence ker (ZQMorph (V,W)) = (Omega). W ; :: thesis: verum