let R be Ring; :: thesis: for V being LeftMod of R

for x being object holds

( x in (0). V iff x = 0. V )

let V be LeftMod of R; :: thesis: for x being object holds

( x in (0). V iff x = 0. V )

let x be object ; :: thesis: ( x in (0). V iff x = 0. V )

thus ( x in (0). V implies x = 0. V ) :: thesis: ( x = 0. V implies x in (0). V )

for x being object holds

( x in (0). V iff x = 0. V )

let V be LeftMod of R; :: thesis: for x being object holds

( x in (0). V iff x = 0. V )

let x be object ; :: thesis: ( x in (0). V iff x = 0. V )

thus ( x in (0). V implies x = 0. V ) :: thesis: ( x = 0. V implies x in (0). V )

proof

thus
( x = 0. V implies x in (0). V )
by ZMODUL01:33; :: thesis: verum
assume
x in (0). V
; :: thesis: x = 0. V

then x in the carrier of ((0). V) ;

then x in {(0. V)} by VECTSP_4:def 3;

hence x = 0. V by TARSKI:def 1; :: thesis: verum

end;then x in the carrier of ((0). V) ;

then x in {(0. V)} by VECTSP_4:def 3;

hence x = 0. V by TARSKI:def 1; :: thesis: verum