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

proof

let x be set ; :: thesis: ( x in { (X (+) B) where X is binary-image of E : X in F } iff x in { ((dilation B) . X) where X is binary-image of E : X in F } )

hereby :: thesis: ( x in { ((dilation B) . X) where X is binary-image of E : X in F } implies x in { (X (+) B) where X is binary-image of E : X in F } )

assume x in { (X (+) B) where X is binary-image of E : X in F } ; :: thesis: x in { ((dilation B) . W) where W is binary-image of E : W in F }
then consider X being binary-image of E such that
P3: ( x = X (+) B & X in F ) ;
( x = (dilation B) . X & X in F ) by P3, def020;
hence x in { ((dilation B) . W) where W is binary-image of E : W in F } ; :: thesis: verum

end;

assume x in { ((dilation B) . X) where X is binary-image of E : X in F } ; :: thesis: x in { (X (+) B) where X is binary-image of E : X in F }
then consider X being binary-image of E such that
P3: ( x = (dilation B) . X & X in F ) ;
( x = X (+) B & X in F ) by P3, def020;
hence x in { (W (+) B) where W is binary-image of E : W in F } ; :: thesis: verum

end;

thus (dilation B) . (union F) = (union F) (+) B by def020
.= union { (X (+) B) where X is binary-image of E : X in F } by Th108B
.= union { ((dilation B) . X) where X is binary-image of E : X in F } by P2, TARSKI:1 ; :: thesis: verum