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 }

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 object st x in A (+) B holds

x in union { (b + A) where b is Element of E : b in B }

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

let x be object ; :: thesis: ( x in A (+) B implies x in union { (b + A) where b is Element of E : b in B } )

assume A1: 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

A2: ( x = a0 + b0 & a0 in A & b0 in B ) by A1;

A3: x in b0 + A by A2;

b0 + A in { (b + A) where b is Element of E : b in B } by A2;

hence x in union { (b + A) where b is Element of E : b in B } by A3, TARSKI:def 4; :: thesis: verum

end;assume A1: 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

A2: ( x = a0 + b0 & a0 in A & b0 in B ) by A1;

A3: x in b0 + A by A2;

b0 + A in { (b + A) where b is Element of E : b in B } by A2;

hence x in union { (b + A) where b is Element of E : b in B } by A3, TARSKI:def 4; :: thesis: verum

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

x in A (+) B

hence
union { (b + A) where b is Element of E : b in B } c= A (+) B
; :: thesis: verumx in A (+) B

let x be object ; :: 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

A4: ( 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

A5: ( y = b + A & b in B ) by A4;

consider a being Element of E such that

A6: ( x = b + a & a in A ) by A5, A4;

thus x in A (+) B by A5, A6; :: thesis: verum

end;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

A4: ( 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

A5: ( y = b + A & b in B ) by A4;

consider a being Element of E such that

A6: ( x = b + a & a in A ) by A5, A4;

thus x in A (+) B by A5, A6; :: thesis: verum