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

for O being Operation of X holds L WHEREeq (O,0) = L WHERE (NOT O)

let L be List of X; :: thesis: for O being Operation of X holds L WHEREeq (O,0) = L WHERE (NOT O)

let O be Operation of X; :: thesis: L WHEREeq (O,0) = L WHERE (NOT O)

thus L WHEREeq (O,0) c= L WHERE (NOT O) :: according to XBOOLE_0:def 10 :: thesis: L WHERE (NOT O) c= L WHEREeq (O,0)

assume z in L WHERE (NOT O) ; :: thesis: z in L WHEREeq (O,0)

then consider x being Element of X such that

A2: ( z = x & ex y being Element of X st

( x,y in NOT O & x in L ) ) ;

consider y being Element of X such that

A3: ( x,y in NOT O & x in L ) by A2;

[x,y] in NOT O by A3;

then ( x = y & x in X & x nin dom O ) by Th36;

then x . O = {} by RELAT_1:170;

then card (x . O) = 0 ;

hence z in L WHEREeq (O,0) by A2; :: thesis: verum

for O being Operation of X holds L WHEREeq (O,0) = L WHERE (NOT O)

let L be List of X; :: thesis: for O being Operation of X holds L WHEREeq (O,0) = L WHERE (NOT O)

let O be Operation of X; :: thesis: L WHEREeq (O,0) = L WHERE (NOT O)

thus L WHEREeq (O,0) c= L WHERE (NOT O) :: according to XBOOLE_0:def 10 :: thesis: L WHERE (NOT O) c= L WHEREeq (O,0)

proof

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

assume z in L WHEREeq (O,0) ; :: thesis: z in L WHERE (NOT O)

then consider x being Element of X such that

A1: ( z = x & card (x . O) = 0 & x in L ) ;

x . O = {} by A1;

then x nin dom O by RELAT_1:170;

then [x,x] in NOT O by A1, Th36;

then x,x in NOT O ;

hence z in L WHERE (NOT O) by A1; :: thesis: verum

end;assume z in L WHEREeq (O,0) ; :: thesis: z in L WHERE (NOT O)

then consider x being Element of X such that

A1: ( z = x & card (x . O) = 0 & x in L ) ;

x . O = {} by A1;

then x nin dom O by RELAT_1:170;

then [x,x] in NOT O by A1, Th36;

then x,x in NOT O ;

hence z in L WHERE (NOT O) by A1; :: thesis: verum

assume z in L WHERE (NOT O) ; :: thesis: z in L WHEREeq (O,0)

then consider x being Element of X such that

A2: ( z = x & ex y being Element of X st

( x,y in NOT O & x in L ) ) ;

consider y being Element of X such that

A3: ( x,y in NOT O & x in L ) by A2;

[x,y] in NOT O by A3;

then ( x = y & x in X & x nin dom O ) by Th36;

then x . O = {} by RELAT_1:170;

then card (x . O) = 0 ;

hence z in L WHEREeq (O,0) by A2; :: thesis: verum