let X be set ; :: thesis: for L1, L2 being List of X

for O being Operation of X st L1 <> {} & L1 c= L2 holds

L2 \& O c= L1 \& O

let L1, L2 be List of X; :: thesis: for O being Operation of X st L1 <> {} & L1 c= L2 holds

L2 \& O c= L1 \& O

let O be Operation of X; :: thesis: ( L1 <> {} & L1 c= L2 implies L2 \& O c= L1 \& O )

assume A1: L1 <> {} ; :: thesis: ( not L1 c= L2 or L2 \& O c= L1 \& O )

assume A2: L1 c= L2 ; :: thesis: L2 \& O c= L1 \& O

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in L2 \& O or z in L1 \& O )

assume A3: z in L2 \& O ; :: thesis: z in L1 \& O

for O being Operation of X st L1 <> {} & L1 c= L2 holds

L2 \& O c= L1 \& O

let L1, L2 be List of X; :: thesis: for O being Operation of X st L1 <> {} & L1 c= L2 holds

L2 \& O c= L1 \& O

let O be Operation of X; :: thesis: ( L1 <> {} & L1 c= L2 implies L2 \& O c= L1 \& O )

assume A1: L1 <> {} ; :: thesis: ( not L1 c= L2 or L2 \& O c= L1 \& O )

assume A2: L1 c= L2 ; :: thesis: L2 \& O c= L1 \& O

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in L2 \& O or z in L1 \& O )

assume A3: z in L2 \& O ; :: thesis: z in L1 \& O

now :: thesis: ( { (x . O) where x is Element of X : x in L1 } <> {} & ( for Y being set st Y in { (x . O) where x is Element of X : x in L1 } holds

z in Y ) )

hence
z in L1 \& O
by SETFAM_1:def 1; :: thesis: verumz in Y ) )

set c = the Element of L1;

the Element of L1 in L1 by A1;

then reconsider c = the Element of L1 as Element of X ;

c . O in { (x . O) where x is Element of X : x in L1 } by A1;

hence { (x . O) where x is Element of X : x in L1 } <> {} ; :: thesis: for Y being set st Y in { (x . O) where x is Element of X : x in L1 } holds

z in Y

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

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

then consider x being Element of X such that

A4: ( Y = x . O & x in L1 ) ;

Y in { (a . O) where a is Element of X : a in L2 } by A4, A2;

hence z in Y by A3, SETFAM_1:def 1; :: thesis: verum

end;the Element of L1 in L1 by A1;

then reconsider c = the Element of L1 as Element of X ;

c . O in { (x . O) where x is Element of X : x in L1 } by A1;

hence { (x . O) where x is Element of X : x in L1 } <> {} ; :: thesis: for Y being set st Y in { (x . O) where x is Element of X : x in L1 } holds

z in Y

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

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

then consider x being Element of X such that

A4: ( Y = x . O & x in L1 ) ;

Y in { (a . O) where a is Element of X : a in L2 } by A4, A2;

hence z in Y by A3, SETFAM_1:def 1; :: thesis: verum