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

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

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

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

A1: for x being object holds

( x in { (X (+) A) where X is binary-image of E : X in F } iff x in { (A (+) X) where X is binary-image of E : X in F } )

.= union { (X (+) A) where X is binary-image of E : X in F } by Th12

.= union { (A (+) X) where X is binary-image of E : X in F } by A1, TARSKI:2 ; :: thesis: verum

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

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

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

A1: for x being object holds

( x in { (X (+) A) where X is binary-image of E : X in F } iff x in { (A (+) X) where X is binary-image of E : X in F } )

proof

thus A (+) (union F) =
(union F) (+) A
let x be object ; :: thesis: ( x in { (X (+) A) where X is binary-image of E : X in F } iff x in { (A (+) X) where X is binary-image of E : X in F } )

then consider W being binary-image of E such that

A3: ( x = A (+) W & W in F ) ;

( x = W (+) A & W in F ) by A3;

hence x in { (X (+) A) where X is binary-image of E : X in F } ; :: thesis: verum

end;hereby :: thesis: ( x in { (A (+) X) where X is binary-image of E : X in F } implies x in { (X (+) A) where X is binary-image of E : X in F } )

assume
x in { (A (+) X) where X is binary-image of E : X in F }
; :: thesis: x in { (X (+) A) where X is binary-image of E : X in F } assume
x in { (X (+) A) where X is binary-image of E : X in F }
; :: thesis: x in { (A (+) X) where X is binary-image of E : X in F }

then consider W being binary-image of E such that

A2: ( x = W (+) A & W in F ) ;

( x = A (+) W & W in F ) by A2;

hence x in { (A (+) X) where X is binary-image of E : X in F } ; :: thesis: verum

end;then consider W being binary-image of E such that

A2: ( x = W (+) A & W in F ) ;

( x = A (+) W & W in F ) by A2;

hence x in { (A (+) X) where X is binary-image of E : X in F } ; :: thesis: verum

then consider W being binary-image of E such that

A3: ( x = A (+) W & W in F ) ;

( x = W (+) A & W in F ) by A3;

hence x in { (X (+) A) where X is binary-image of E : X in F } ; :: thesis: verum

.= union { (X (+) A) where X is binary-image of E : X in F } by Th12

.= union { (A (+) X) where X is binary-image of E : X in F } by A1, TARSKI:2 ; :: thesis: verum