let V be ComplexLinearSpace; :: thesis: for v being VECTOR of V holds v + ((0). V) = {v}
let v be VECTOR 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 VECTOR of V such that
A1: x = v + u and
A2: u in (0). V ;
A3: the carrier of ((0). V) = {(0. V)} by Def9;
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 Th36, RLVECT_1:4;
hence x in v + ((0). V) by A4; :: thesis: verum