let GF be non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr ; :: thesis: for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF
for v being Element of V holds v + ((0). V) = {v}
let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF; :: thesis: for v being Element of V holds v + ((0). V) = {v}
let v be Element of V; :: thesis: v + ((0). V) = {v}
thus v + ((0). V) c= {v} :: according to XBOOLE_0:def 10 :: thesis: {v} c= v + ((0). V)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in v + ((0). V) or x in {v} )
assume x in v + ((0). V) ; :: thesis: x in {v}
then consider u being Element of V such that
A1: x = v + u and
A2: u in (0). V ;
A3: the carrier of ((0). V) = {(0. V)} by Def3;
u in the carrier of ((0). V) by A2;
then u = 0. V by A3, TARSKI:def 1;
then x = v by A1, RLVECT_1:4;
hence x in {v} by TARSKI:def 1; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {v} or x in v + ((0). V) )
assume x in {v} ; :: thesis: x in v + ((0). V)
then A4: x = v by TARSKI:def 1;
( 0. V in (0). V & v = v + (0. V) ) by Th17, RLVECT_1:4;
hence x in v + ((0). V) by A4; :: thesis: verum