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