let F, H be ZF-formula; :: thesis: for x, y being Variable holds
( 'not' F = ('not' H) / (x,y) iff F = H / (x,y) )
let x, y be Variable; :: thesis: ( 'not' F = ('not' H) / (x,y) iff F = H / (x,y) )
set N = ('not' H) / (x,y);
A1: len <*2*> = 1 by FINSEQ_1:39;
A2: ( dom ('not' F) = Seg (len ('not' F)) & dom ('not' H) = Seg (len ('not' H)) ) by FINSEQ_1:def 3;
A3: ( len ('not' F) = (len <*2*>) + (len F) & len ('not' H) = (len <*2*>) + (len H) ) by FINSEQ_1:22;
A4: ( dom F = Seg (len F) & dom H = Seg (len H) ) by FINSEQ_1:def 3;
thus ( 'not' F = ('not' H) / (x,y) implies F = H / (x,y) ) :: thesis: ( F = H / (x,y) implies 'not' F = ('not' H) / (x,y) )

proof

assume A5: 'not' F = ('not' H) / (x,y) ; :: thesis: F = H / (x,y)
then A6: dom ('not' F) = dom ('not' H) by Def3;
then A7: len ('not' F) = len ('not' H) by FINSEQ_3:29;

A8: now :: thesis: for a being object st a in dom F holds
F . a = (H / (x,y)) . a

let a be object ; :: thesis: ( a in dom F implies F . a = (H / (x,y)) . a )
assume A9: a in dom F ; :: thesis: F . a = (H / (x,y)) . a
then reconsider i = a as Element of NAT ;
A10: ( F . a = (('not' H) / (x,y)) . (1 + i) & 1 + i in dom (('not' H) / (x,y)) ) by A1, A5, A9, FINSEQ_1:28, FINSEQ_1:def 7;
A11: ('not' H) . (1 + i) = H . a by A1, A4, A3, A7, A9, FINSEQ_1:def 7;
then A12: ( H . a = x implies F . a = y ) by A5, A6, A10, Def3;
A13: ( H . a <> x implies F . a = H . a ) by A5, A6, A10, A11, Def3;
( H . a = x implies (H / (x,y)) . a = y ) by A4, A3, A7, A9, Def3;
hence F . a = (H / (x,y)) . a by A4, A3, A7, A9, A12, A13, Def3; :: thesis: verum

end;

A14: dom H = dom (H / (x,y)) by Def3;
dom F = dom H by A3, A7, FINSEQ_3:29;
hence F = H / (x,y) by A14, A8, FUNCT_1:2; :: thesis: verum

end;

assume A15: F = H / (x,y) ; :: thesis: 'not' F = ('not' H) / (x,y)
then A16: dom F = dom H by Def3;
then A17: len F = len H by FINSEQ_3:29;
A18: dom <*2*> = {1} by FINSEQ_1:2, FINSEQ_1:def 8;

A19: now :: thesis: for a being object st a in dom ('not' F) holds
('not' F) . a = (('not' H) / (x,y)) . a

let a be object ; :: thesis: ( a in dom ('not' F) implies ('not' F) . a = (('not' H) / (x,y)) . a )
assume A20: a in dom ('not' F) ; :: thesis: ('not' F) . a = (('not' H) / (x,y)) . a
then reconsider i = a as Element of NAT ;

A21: now :: thesis: ( ex j being Nat st
( j in dom F & i = 1 + j ) implies ('not' F) . a = (('not' H) / (x,y)) . a )

A22: ( ('not' H) . a <> x implies (('not' H) / (x,y)) . a = ('not' H) . a ) by A2, A3, A17, A20, Def3;
given j being Nat such that A23: j in dom F and
A24: i = 1 + j ; :: thesis: ('not' F) . a = (('not' H) / (x,y)) . a
A25: ( H . j = ('not' H) . i & F . j = ('not' F) . i ) by A1, A16, A23, A24, FINSEQ_1:def 7;
then A26: ( ('not' H) . a = x implies ('not' F) . a = y ) by A15, A16, A23, Def3;
( ('not' H) . a <> x implies ('not' F) . a = ('not' H) . a ) by A15, A16, A23, A25, Def3;
hence ('not' F) . a = (('not' H) / (x,y)) . a by A2, A3, A17, A20, A26, A22, Def3; :: thesis: verum

end;

now :: thesis: ( i in {1} implies ('not' F) . a = (('not' H) / (x,y)) . a )

A27: ( ('not' H) . 1 = 2 & 2 <> x ) by Th135, FINSEQ_1:41;
assume i in {1} ; :: thesis: ('not' F) . a = (('not' H) / (x,y)) . a
then A28: i = 1 by TARSKI:def 1;
then ('not' F) . i = 2 by FINSEQ_1:41;
hence ('not' F) . a = (('not' H) / (x,y)) . a by A2, A3, A17, A20, A28, A27, Def3; :: thesis: verum

end;

hence ('not' F) . a = (('not' H) / (x,y)) . a by A1, A18, A20, A21, FINSEQ_1:25; :: thesis: verum

end;

dom ('not' F) = dom (('not' H) / (x,y)) by A2, A3, A17, Def3;
hence 'not' F = ('not' H) / (x,y) by A19, FUNCT_1:2; :: thesis: verum