let X be set ; :: thesis: for x being Element of X

for O1, O2 being Operation of X holds x . (O1 \& O2) = (x . O1) \& O2

let x be Element of X; :: thesis: for O1, O2 being Operation of X holds x . (O1 \& O2) = (x . O1) \& O2

let O1, O2 be Operation of X; :: thesis: x . (O1 \& O2) = (x . O1) \& O2

for O1, O2 being Operation of X holds x . (O1 \& O2) = (x . O1) \& O2

let x be Element of X; :: thesis: for O1, O2 being Operation of X holds x . (O1 \& O2) = (x . O1) \& O2

let O1, O2 be Operation of X; :: thesis: x . (O1 \& O2) = (x . O1) \& O2

per cases
( X = {} or X <> {} )
;

end;

suppose
X = {}
; :: thesis: x . (O1 \& O2) = (x . O1) \& O2

then
( x . (O1 \& O2) = {} & (x . O1) \& O2 = {} )
;

hence x . (O1 \& O2) = (x . O1) \& O2 ; :: thesis: verum

end;hence x . (O1 \& O2) = (x . O1) \& O2 ; :: thesis: verum

suppose
X <> {}
; :: thesis: x . (O1 \& O2) = (x . O1) \& O2

then reconsider L = {x} as List of X by ZFMISC_1:31;

A1: { ((a . O1) \& O2) where a is Element of X : a in L } = {((x . O1) \& O2)}

.= (x . O1) \& O2 by A1, ZFMISC_1:25 ; :: thesis: verum

end;A1: { ((a . O1) \& O2) where a is Element of X : a in L } = {((x . O1) \& O2)}

proof

thus x . (O1 \& O2) =
union { ((a . O1) \& O2) where a is Element of X : a in L }
by Def20
thus
{ ((a . O1) \& O2) where a is Element of X : a in L } c= {((x . O1) \& O2)}
:: according to XBOOLE_0:def 10 :: thesis: {((x . O1) \& O2)} c= { ((a . O1) \& O2) where a is Element of X : a in L }

assume z in {((x . O1) \& O2)} ; :: thesis: z in { ((a . O1) \& O2) where a is Element of X : a in L }

then ( z = (x . O1) \& O2 & x in L ) by TARSKI:def 1;

hence z in { ((a . O1) \& O2) where a is Element of X : a in L } ; :: thesis: verum

end;proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in {((x . O1) \& O2)} or z in { ((a . O1) \& O2) where a is Element of X : a in L } )
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in { ((a . O1) \& O2) where a is Element of X : a in L } or z in {((x . O1) \& O2)} )

assume z in { ((a . O1) \& O2) where a is Element of X : a in L } ; :: thesis: z in {((x . O1) \& O2)}

then consider a being Element of X such that

A2: ( z = (a . O1) \& O2 & a in L ) ;

a = x by A2, TARSKI:def 1;

hence z in {((x . O1) \& O2)} by A2, TARSKI:def 1; :: thesis: verum

end;assume z in { ((a . O1) \& O2) where a is Element of X : a in L } ; :: thesis: z in {((x . O1) \& O2)}

then consider a being Element of X such that

A2: ( z = (a . O1) \& O2 & a in L ) ;

a = x by A2, TARSKI:def 1;

hence z in {((x . O1) \& O2)} by A2, TARSKI:def 1; :: thesis: verum

assume z in {((x . O1) \& O2)} ; :: thesis: z in { ((a . O1) \& O2) where a is Element of X : a in L }

then ( z = (x . O1) \& O2 & x in L ) by TARSKI:def 1;

hence z in { ((a . O1) \& O2) where a is Element of X : a in L } ; :: thesis: verum

.= (x . O1) \& O2 by A1, ZFMISC_1:25 ; :: thesis: verum