let E be RealLinearSpace; :: thesis: for A, B being binary-image of E holds A (+) B = union { (b + A) where b is Element of E : b in B }
let A, B be binary-image of E; :: thesis: A (+) B = union { (b + A) where b is Element of E : b in B }

now :: thesis: for x being set st x in A (+) B holds
x in union { (b + A) where b is Element of E : b in B }

let x be set ; :: thesis: ( x in A (+) B implies x in union { (b + A) where b is Element of E : b in B } )
assume P1: x in A (+) B ; :: thesis: x in union { (b + A) where b is Element of E : b in B }
consider a0, b0 being Element of E such that
P2: ( x = a0 + b0 & a0 in A & b0 in B ) by P1;
P3: x in b0 + A by P2;
b0 + A in { (b + A) where b is Element of E : b in B } by P2;
hence x in union { (b + A) where b is Element of E : b in B } by P3, TARSKI:def 4; :: thesis: verum

end;

hence A (+) B c= union { (b + A) where b is Element of E : b in B } by TARSKI:def 3; :: according to XBOOLE_0:def 10 :: thesis: union { (b + A) where b is Element of E : b in B } c= A (+) B

now :: thesis: for x being set st x in union { (b + A) where b is Element of E : b in B } holds
x in A (+) B

let x be set ; :: thesis: ( x in union { (b + A) where b is Element of E : b in B } implies x in A (+) B )
assume x in union { (b + A) where b is Element of E : b in B } ; :: thesis: x in A (+) B
then consider y being set such that
P0: ( x in y & y in { (b + A) where b is Element of E : b in B } ) by TARSKI:def 4;
consider b being Element of E such that
P1: ( y = b + A & b in B ) by P0;
consider a being Element of E such that
P2: ( x = b + a & a in A ) by P1, P0;
thus x in A (+) B by P1, P2; :: thesis: verum

end;

hence union { (b + A) where b is Element of E : b in B } c= A (+) B by TARSKI:def 3; :: thesis: verum