let V be Z_Module; :: thesis: for W being Submodule of V holds ker (ZQMorph (V,W)) = (Omega). W
let W be Submodule of V; :: thesis: ker (ZQMorph (V,W)) = (Omega). W
set f = ZQMorph (V,W);
reconsider Ws = (Omega). W as strict Submodule of V by ZMODUL01:42;
for x being object holds
( x in (ZQMorph (V,W)) " {(0. (Z_ModuleQuot (V,W)))} iff x in the carrier of W )

proof

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

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

assume A11: x in (ZQMorph (V,W)) " {(0. (Z_ModuleQuot (V,W)))} ; :: thesis: x in the carrier of W
then A1: ( x in the carrier of V & (ZQMorph (V,W)) . x in {(0. (Z_ModuleQuot (V,W)))} ) by FUNCT_2:38;
reconsider v = x as VECTOR of V by A11;
(ZQMorph (V,W)) . v = 0. (Z_ModuleQuot (V,W)) by A1, TARSKI:def 1
.= zeroCoset (V,W) by ZMODUL02:def 10
.= the carrier of W ;
then v + W = the carrier of W by defMophVW;
then v in W by ZMODUL01:63;
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. (Z_ModuleQuot (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, ZMODUL01:63
.= 0. (Z_ModuleQuot (V,W)) by ZMODUL02:def 10 ;
then (ZQMorph (V,W)) . x in {(0. (Z_ModuleQuot (V,W)))} by TARSKI:def 1;
hence x in (ZQMorph (V,W)) " {(0. (Z_ModuleQuot (V,W)))} by B1, B4, FUNCT_2:38; :: thesis: verum

end;

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