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 )

proof

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;

assume A7: ( z = s & z in X & z nin dom O ) ; :: thesis: [z,s] in NOT O
then reconsider z = z as Element of X ;
z . O c= {}

proof

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;

then z . O = {} ;
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