let X be set ; :: thesis: for L being List of X

for O1, O2 being Operation of X st O1 c= O2 holds

L \& O1 c= L \& O2

let L be List of X; :: thesis: for O1, O2 being Operation of X st O1 c= O2 holds

L \& O1 c= L \& O2

let O1, O2 be Operation of X; :: thesis: ( O1 c= O2 implies L \& O1 c= L \& O2 )

assume A1: O1 c= O2 ; :: thesis: L \& O1 c= L \& O2

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in L \& O1 or z in L \& O2 )

assume A2: z in L \& O1 ; :: thesis: z in L \& O2

then { (x . O1) where x is Element of X : x in L } <> {} by SETFAM_1:def 1;

then consider Y being object such that

A3: Y in { (x . O1) where x is Element of X : x in L } by XBOOLE_0:def 1;

consider y being Element of X such that

A4: ( Y = y . O1 & y in L ) by A3;

A5: y . O2 in { (x . O2) where x is Element of X : x in L } by A4;

for O1, O2 being Operation of X st O1 c= O2 holds

L \& O1 c= L \& O2

let L be List of X; :: thesis: for O1, O2 being Operation of X st O1 c= O2 holds

L \& O1 c= L \& O2

let O1, O2 be Operation of X; :: thesis: ( O1 c= O2 implies L \& O1 c= L \& O2 )

assume A1: O1 c= O2 ; :: thesis: L \& O1 c= L \& O2

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in L \& O1 or z in L \& O2 )

assume A2: z in L \& O1 ; :: thesis: z in L \& O2

then { (x . O1) where x is Element of X : x in L } <> {} by SETFAM_1:def 1;

then consider Y being object such that

A3: Y in { (x . O1) where x is Element of X : x in L } by XBOOLE_0:def 1;

consider y being Element of X such that

A4: ( Y = y . O1 & y in L ) by A3;

A5: y . O2 in { (x . O2) where x is Element of X : x in L } by A4;

now :: thesis: for Y being set st Y in { (x . O2) where x is Element of X : x in L } holds

z in Y

hence
z in L \& O2
by A5, SETFAM_1:def 1; :: thesis: verumz in Y

let Y be set ; :: thesis: ( Y in { (x . O2) where x is Element of X : x in L } implies z in Y )

assume Y in { (x . O2) where x is Element of X : x in L } ; :: thesis: z in Y

then consider a being Element of X such that

A6: ( Y = a . O2 & a in L ) ;

a . O1 in { (x . O1) where x is Element of X : x in L } by A6;

then ( z in a . O1 & a . O1 c= Y ) by A1, A2, A6, Th1, SETFAM_1:def 1;

hence z in Y ; :: thesis: verum

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

then consider a being Element of X such that

A6: ( Y = a . O2 & a in L ) ;

a . O1 in { (x . O1) where x is Element of X : x in L } by A6;

then ( z in a . O1 & a . O1 c= Y ) by A1, A2, A6, Th1, SETFAM_1:def 1;

hence z in Y ; :: thesis: verum