let E be RealLinearSpace; :: thesis: for A, B being non empty binary-image of E holds A (+) B = { v where v is Element of E : (v + ((- 1) * B)) /\ A <> {} }
let A, B be non empty binary-image of E; :: thesis: A (+) B = { v where v is Element of E : (v + ((- 1) * B)) /\ A <> {} }
thus A (+) B c= { v where v is Element of E : (v + ((- 1) * B)) /\ A <> {} } :: according to XBOOLE_0:def 10 :: thesis: { v where v is Element of E : (v + ((- 1) * B)) /\ A <> {} } c= A (+) B

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in A (+) B or x in { v where v is Element of E : (v + ((- 1) * B)) /\ A <> {} } )
assume P1: x in A (+) B ; :: thesis: x in { v where v is Element of E : (v + ((- 1) * B)) /\ A <> {} }
consider a0, b0 being Element of E such that
P2: ( x = a0 + b0 & a0 in A & b0 in B ) by P1;
reconsider v = x as Element of E by P1;
P3: v - b0 = a0 by P2, RLVECT_4:1;
(- 1) * b0 in (- 1) * B by P2;
then v + ((- 1) * b0) in v + ((- 1) * B) ;
then v - b0 in v + ((- 1) * B) by RLVECT_1:16;
then (v + ((- 1) * B)) /\ A <> {} by P2, P3, XBOOLE_0:def 4;
hence x in { w where w is Element of E : (w + ((- 1) * B)) /\ A <> {} } ; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { v where v is Element of E : (v + ((- 1) * B)) /\ A <> {} } or x in A (+) B )
assume x in { v where v is Element of E : (v + ((- 1) * B)) /\ A <> {} } ; :: thesis: x in A (+) B
then consider v being Element of E such that
P1: ( x = v & (v + ((- 1) * B)) /\ A <> {} ) ;
consider y being set such that
X1: y in (v + ((- 1) * B)) /\ A by P1, XBOOLE_0:def 1;
X2: ( y in v + ((- 1) * B) & y in A ) by X1, XBOOLE_0:def 4;
then consider nb being Element of E such that
X3: ( y = v + nb & nb in (- 1) * B ) ;
consider b being Element of E such that
X4: ( nb = (- 1) * b & b in B ) by X3;
reconsider a = y as Element of E by X3;
a + b = (v - b) + b by X3, X4, RLVECT_1:16
.= v by RLVECT_4:1 ;
hence x in A (+) B by P1, X4, X2; :: thesis: verum