let x be set ; :: thesis: for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr of GF holds
( x in (0). V iff x = 0. V )
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; :: thesis: for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr of GF holds
( x in (0). V iff x = 0. V )
let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr of GF; :: 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

assume x in (0). V ; :: thesis: x = 0. V
then x in the carrier of ((0). V) by STRUCT_0:def 5;
then x in {(0. V)} by Def3;
hence x = 0. V by TARSKI:def 1; :: thesis: verum

end;

thus ( x = 0. V implies x in (0). V ) by Th25; :: thesis: verum