let E be RealLinearSpace; :: thesis: for F being binary-image-family of E
for B being non empty binary-image of E holds (union F) (+) 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 (union F) (+) B = union { (X (+) B) where X is binary-image of E : X in F }
let B be non empty binary-image of E; :: thesis: (union F) (+) B = union { (X (+) B) where X is binary-image of E : X in F }
for x being object holds
( x in (union F) (+) 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 (union F) (+) 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 (union F) (+) B )

assume x in (union F) (+) 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 A1, TARSKI:def 4;
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 A3, TARSKI:def 4; :: thesis: verum

end;

assume x in union { (X (+) B) where X is binary-image of E : X in F } ; :: thesis: x in (union F) (+) 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 A5, ZFMISC_1:74;
hence x in (union F) (+) 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