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) 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 { (() . X) where X is binary-image of E : X in F }
let B be non empty binary-image of E; :: thesis: () . () = union { (() . X) where X is binary-image of E : X in F }
A1: for x being object holds
( x in { (X (+) B) where X is binary-image of E : X in F } iff x in { (() . X) where X is binary-image of E : X in F } )
proof
let x be object ; :: thesis: ( x in { (X (+) B) where X is binary-image of E : X in F } iff x in { (() . X) where X is binary-image of E : X in F } )
hereby :: thesis: ( x in { (() . 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 { (() . W) where W is binary-image of E : W in F }
then consider X being binary-image of E such that
A2: ( x = X (+) B & X in F ) ;
( x = () . X & X in F ) by ;
hence x in { (() . W) where W is binary-image of E : W in F } ; :: thesis: verum
end;
assume x in { (() . 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
A3: ( x = () . X & X in F ) ;
( x = X (+) B & X in F ) by ;
hence x in { (W (+) B) where W is binary-image of E : W in F } ; :: thesis: verum
end;
thus () . () = () (+) B by Def2
.= union { (X (+) B) where X is binary-image of E : X in F } by Th12
.= union { (() . X) where X is binary-image of E : X in F } by ; :: thesis: verum