let E be RealLinearSpace; :: thesis: for F being binary-image-family of E

for B being non empty binary-image of E holds union { (X (-) B) where X is binary-image of E : X in F } c= (union F) (-) B

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

let B be non empty binary-image of E; :: thesis: union { (X (-) B) where X is binary-image of E : X in F } c= (union F) (-) B

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union { (X (-) B) where X is binary-image of E : X in F } or 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) (-) B

then consider Y being set such that

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

A2: ( Y = W (-) B & W in F ) by A1;

consider z being Element of E such that

A3: ( x = z & ( for b being Element of E st b in B holds

z - b in W ) ) by A1, A2;

for B being non empty binary-image of E holds union { (X (-) B) where X is binary-image of E : X in F } c= (union F) (-) B

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

let B be non empty binary-image of E; :: thesis: union { (X (-) B) where X is binary-image of E : X in F } c= (union F) (-) B

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union { (X (-) B) where X is binary-image of E : X in F } or 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) (-) B

then consider Y being set such that

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

A2: ( Y = W (-) B & W in F ) by A1;

consider z being Element of E such that

A3: ( x = z & ( for b being Element of E st b in B holds

z - b in W ) ) by A1, A2;

now :: thesis: for b being Element of E st b in B holds

z - b in union F

hence
x in (union F) (-) B
by A3; :: thesis: verumz - b in union F

let b be Element of E; :: thesis: ( b in B implies z - b in union F )

assume b in B ; :: thesis: z - b in union F

then A4: z - b in W by A3;

W c= union F by A2, ZFMISC_1:74;

hence z - b in union F by A4; :: thesis: verum

end;assume b in B ; :: thesis: z - b in union F

then A4: z - b in W by A3;

W c= union F by A2, ZFMISC_1:74;

hence z - b in union F by A4; :: thesis: verum