let z, s, X be set ; :: thesis: for O being Operation of X holds
( [z,s] in NOT O iff ( z = s & z in X & z nin dom O ) )
let O be Operation of X; :: 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] 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 DEFNOT;
then consider Y being set such that
A1: ( 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
A2: ( Y = IFEQ ((x . O),{},{x},{}) & x in {z} ) by A1;
A3: x = z by A2, TARSKI:def 1;
A5: x . O = {} by A1, A2, FUNCOP_1:def 8;
then s in {x} by A1, A2, FUNCOP_1:def 8;
then ( s = x & ( for s being set holds [x,s] nin O ) ) by A5, RELAT_1:169, TARSKI:def 1;
hence ( z = s & z in X & z nin dom O ) by A3, A7, XTUPLE_0:def 12, ZFMISC_1:87; :: thesis: verum

end;

assume A6: ( 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 set ; :: 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 A6, XTUPLE_0:def 12; :: thesis: verum

end;

then z . O = {} ;
then A7: IFEQ ((z . O),{},{z},{}) = {z} by FUNCOP_1:def 8;
A8: z in {z} by TARSKI:def 1;
reconsider L = {z} as Subset of X by A6, ZFMISC_1:31;
{z} in { (IFEQ ((x . O),{},{x},{})) where x is Element of X : x in {z} } by A7, A8;
then z in union { (IFEQ ((x . O),{},{x},{})) where x is Element of X : x in {z} } by A8, TARSKI:def 4;
then z in L | (NOT O) by DEFNOT;
then z in z . (NOT O) ;
hence [z,s] in NOT O by A6, RELAT_1:169; :: thesis: verum