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 object st x in A (+) B holds
x 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;
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 (+) B
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
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;
hence union { (b + A) where b is Element of E : b in B } c= A (+) B ; :: thesis: verum