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
per cases ( X = {} or X <> {} ) ;
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;
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)}
proof
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 }
proof
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;
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 } )
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;
thus x . (O1 \& O2) = union { ((a . O1) \& O2) where a is Element of X : a in L } by Def20
.= (x . O1) \& O2 by A1, ZFMISC_1:25 ; :: thesis: verum
end;
end;