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;

now :: thesis: for Y being set st Y in { (x . O2) where x is Element of X : x in L } holds
z 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;

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