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

for O being Operation of X holds L WHEREge (O,1) = L WHERE O

let L be List of X; :: thesis: for O being Operation of X holds L WHEREge (O,1) = L WHERE O

let O be Operation of X; :: thesis: L WHEREge (O,1) = L WHERE O

thus L WHEREge (O,1) c= L WHERE O by Th6; :: according to XBOOLE_0:def 10 :: thesis: L WHERE O c= L WHEREge (O,1)

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in L WHERE O or z in L WHEREge (O,1) )

assume A1: z in L WHERE O ; :: thesis: z in L WHEREge (O,1)

then reconsider z = z as Element of X ;

A2: ( z . O <> {} & z in L ) by A1, Th3;

then succ 0 c= card (z . O) by ORDINAL1:21, ORDINAL3:8;

hence z in L WHEREge (O,1) by A2; :: thesis: verum

for O being Operation of X holds L WHEREge (O,1) = L WHERE O

let L be List of X; :: thesis: for O being Operation of X holds L WHEREge (O,1) = L WHERE O

let O be Operation of X; :: thesis: L WHEREge (O,1) = L WHERE O

thus L WHEREge (O,1) c= L WHERE O by Th6; :: according to XBOOLE_0:def 10 :: thesis: L WHERE O c= L WHEREge (O,1)

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in L WHERE O or z in L WHEREge (O,1) )

assume A1: z in L WHERE O ; :: thesis: z in L WHEREge (O,1)

then reconsider z = z as Element of X ;

A2: ( z . O <> {} & z in L ) by A1, Th3;

then succ 0 c= card (z . O) by ORDINAL1:21, ORDINAL3:8;

hence z in L WHEREge (O,1) by A2; :: thesis: verum