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 } )

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

hence
(union F) (+) B = union { (X (+) B) where X is binary-image of E : X in F }
by TARSKI:2; :: thesis: verum
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 } )

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

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