let E be RealLinearSpace; :: thesis: for F being binary-image-family of E
for B being non empty binary-image of E holds () (+) B = union { (X (+) B) where X is binary-image of E : X in F }

let F be binary-image-family of E; :: thesis: for B being non empty binary-image of E holds () (+) B = union { (X (+) B) where X is binary-image of E : X in F }
let B be non empty binary-image of E; :: thesis: () (+) B = union { (X (+) B) where X is binary-image of E : X in F }
for x being object holds
( x in () (+) B iff x in union { (X (+) B) where X is binary-image of E : X in F } )
proof
let x be object ; :: thesis: ( x in () (+) B iff x in union { (X (+) B) where X is binary-image of E : X in F } )
hereby :: thesis: ( x in union { (X (+) B) where X is binary-image of E : X in F } implies x in () (+) B )
assume x in () (+) B ; :: thesis: x in union { (W (+) B) where W is binary-image of E : W in F }
then consider f, b being Element of E such that
A1: ( x = f + b & f in union F & b in B ) ;
consider Y being set such that
A2: ( f in Y & Y in F ) by ;
reconsider X = Y as binary-image of E by A2;
A3: x in X (+) B by A1, A2;
X (+) B in { (W (+) B) where W is binary-image of E : W in F } by A2;
hence x in union { (W (+) B) where W is binary-image of E : W in F } by ; :: thesis: verum
end;
assume x in union { (X (+) B) where X is binary-image of E : X in F } ; :: thesis: x in () (+) B
then consider Y being set such that
A4: ( x in Y & Y in { (X (+) B) where X is binary-image of E : X in F } ) by TARSKI:def 4;
consider W being binary-image of E such that
A5: ( Y = W (+) B & W in F ) by A4;
consider f, b being Element of E such that
A6: ( x = f + b & f in W & b in B ) by A4, A5;
W c= union F by ;
hence x in () (+) B by A6; :: thesis: verum
end;
hence (union F) (+) B = union { (X (+) B) where X is binary-image of E : X in F } by TARSKI:2; :: thesis: verum