let R be Ring; :: thesis: for V being LeftMod of R holds Lin {(0. V)} = (0). V
let V be LeftMod of R; :: thesis: Lin {(0. V)} = (0). V
for x being object holds
( x in Lin {(0. V)} iff x in (0). V )

proof

let x be object ; :: thesis: ( x in Lin {(0. V)} iff x in (0). V )

hereby :: thesis: ( x in (0). V implies x in Lin {(0. V)} )

assume x in Lin {(0. V)} ; :: thesis: x in (0). V
then consider l being Linear_Combination of {(0. V)} such that
B2: x = Sum l by MOD_3:4;
Sum l = (l . (0. V)) * (0. V) by VECTSP_6:17
.= 0. V by VECTSP_1:14 ;
hence x in (0). V by B2, VECTSP_4:17; :: thesis: verum

end;

assume x in (0). V ; :: thesis: x in Lin {(0. V)}
then x = 0. V by VECTSP_4:35;
hence x in Lin {(0. V)} by VECTSP_4:17; :: thesis: verum

end;

then for x being Vector of V holds
( x in Lin {(0. V)} iff x in (0). V ) ;
hence Lin {(0. V)} = (0). V by VECTSP_4:30; :: thesis: verum