let X be set ; :: thesis: for O being Operation of X

for z, s being object holds

( [z,s] in NOT O iff ( z = s & z in X & z nin dom O ) )

let O be Operation of X; :: thesis: for z, s being object holds

( [z,s] in NOT O iff ( z = s & z in X & z nin dom O ) )

let z, s be object ; :: thesis: ( [z,s] in NOT O iff ( z = s & z in X & z nin dom O ) )

thus ( [z,s] in NOT O implies ( z = s & z in X & z nin dom O ) ) :: thesis: ( z = s & z in X & z nin dom O implies [z,s] in NOT O )

then reconsider z = z as Element of X ;

z . O c= {}

then A8: IFEQ ((z . O),{},{z},{}) = {z} by FUNCOP_1:def 8;

A9: z in {z} by TARSKI:def 1;

reconsider L = {z} as Subset of X by A7, ZFMISC_1:31;

{z} in { (IFEQ ((x . O),{},{x},{})) where x is Element of X : x in {z} } by A8, A9;

then z in union { (IFEQ ((x . O),{},{x},{})) where x is Element of X : x in {z} } by A9, TARSKI:def 4;

then z in L | (NOT O) by Def15;

then z in z . (NOT O) ;

hence [z,s] in NOT O by A7, RELAT_1:169; :: thesis: verum

for z, s being object holds

( [z,s] in NOT O iff ( z = s & z in X & z nin dom O ) )

let O be Operation of X; :: thesis: for z, s being object holds

( [z,s] in NOT O iff ( z = s & z in X & z nin dom O ) )

let z, s be object ; :: thesis: ( [z,s] in NOT O iff ( z = s & z in X & z nin dom O ) )

thus ( [z,s] in NOT O implies ( z = s & z in X & z nin dom O ) ) :: thesis: ( z = s & z in X & z nin dom O implies [z,s] in NOT O )

proof

assume A7:
( z = s & z in X & z nin dom O )
; :: thesis: [z,s] in NOT O
assume A1:
[z,s] in NOT O
; :: thesis: ( z = s & z in X & z nin dom O )

then ( s in Im ((NOT O),z) & z in X ) by RELAT_1:169, ZFMISC_1:87;

then ( s in (NOT O) .: {z} & {z} c= X ) by ZFMISC_1:31;

then s in union { (IFEQ ((x . O),{},{x},{})) where x is Element of X : x in {z} } by Def15;

then consider Y being set such that

A2: ( s in Y & Y in { (IFEQ ((x . O),{},{x},{})) where x is Element of X : x in {z} } ) by TARSKI:def 4;

consider x being Element of X such that

A3: ( Y = IFEQ ((x . O),{},{x},{}) & x in {z} ) by A2;

A4: x = z by A3, TARSKI:def 1;

A5: x . O = {} by A2, A3, FUNCOP_1:def 8;

then s in {x} by A2, A3, FUNCOP_1:def 8;

then A6: ( s = x & ( for s being object holds [x,s] nin O ) ) by A5, RELAT_1:169, TARSKI:def 1;

hence z = s by A4; :: thesis: ( z in X & z nin dom O )

thus z in X by A1, ZFMISC_1:87; :: thesis: z nin dom O

( x in dom O iff ex y being object st [x,y] in O ) by XTUPLE_0:def 12;

hence z nin dom O by A4, A6; :: thesis: verum

end;then ( s in Im ((NOT O),z) & z in X ) by RELAT_1:169, ZFMISC_1:87;

then ( s in (NOT O) .: {z} & {z} c= X ) by ZFMISC_1:31;

then s in union { (IFEQ ((x . O),{},{x},{})) where x is Element of X : x in {z} } by Def15;

then consider Y being set such that

A2: ( s in Y & Y in { (IFEQ ((x . O),{},{x},{})) where x is Element of X : x in {z} } ) by TARSKI:def 4;

consider x being Element of X such that

A3: ( Y = IFEQ ((x . O),{},{x},{}) & x in {z} ) by A2;

A4: x = z by A3, TARSKI:def 1;

A5: x . O = {} by A2, A3, FUNCOP_1:def 8;

then s in {x} by A2, A3, FUNCOP_1:def 8;

then A6: ( s = x & ( for s being object holds [x,s] nin O ) ) by A5, RELAT_1:169, TARSKI:def 1;

hence z = s by A4; :: thesis: ( z in X & z nin dom O )

thus z in X by A1, ZFMISC_1:87; :: thesis: z nin dom O

( x in dom O iff ex y being object st [x,y] in O ) by XTUPLE_0:def 12;

hence z nin dom O by A4, A6; :: thesis: verum

then reconsider z = z as Element of X ;

z . O c= {}

proof

then
z . O = {}
;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in z . O or y in {} )

assume y in z . O ; :: thesis: y in {}

then [z,y] in O by RELAT_1:169;

hence y in {} by A7, XTUPLE_0:def 12; :: thesis: verum

end;assume y in z . O ; :: thesis: y in {}

then [z,y] in O by RELAT_1:169;

hence y in {} by A7, XTUPLE_0:def 12; :: thesis: verum

then A8: IFEQ ((z . O),{},{z},{}) = {z} by FUNCOP_1:def 8;

A9: z in {z} by TARSKI:def 1;

reconsider L = {z} as Subset of X by A7, ZFMISC_1:31;

{z} in { (IFEQ ((x . O),{},{x},{})) where x is Element of X : x in {z} } by A8, A9;

then z in union { (IFEQ ((x . O),{},{x},{})) where x is Element of X : x in {z} } by A9, TARSKI:def 4;

then z in L | (NOT O) by Def15;

then z in z . (NOT O) ;

hence [z,s] in NOT O by A7, RELAT_1:169; :: thesis: verum