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 & dom <*2*> = {1} ) by FINSEQ_1:4, FINSEQ_1:56, FINSEQ_1:def 8;
A2: ( dom ('not' F) = Seg (len ('not' F)) & dom ('not' H) = Seg (len ('not' H)) & dom F = Seg (len F) & dom H = Seg (len H) ) by FINSEQ_1:def 3;
A3: ( len ('not' F) = (len <*2*>) + (len F) & len ('not' H) = (len <*2*>) + (len H) ) by FINSEQ_1:35;
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 A4: 'not' F = ('not' H) / x,y ; :: thesis: F = H / x,y
then dom ('not' F) = dom ('not' H) by Def4;
then A5: len ('not' F) = len ('not' H) by FINSEQ_3:31;
then A6: ( dom H = dom (H / x,y) & dom F = dom H ) by A3, Def4, FINSEQ_3:31;

now

let a be set ; :: thesis: ( a in dom F implies F . a = (H / x,y) . a )
assume A7: a in dom F ; :: thesis: F . a = (H / x,y) . a
then reconsider i = a as Element of NAT ;
( F . a = (('not' H) / x,y) . (1 + i) & 1 + i in dom (('not' H) / x,y) ) by A1, A4, A7, FINSEQ_1:41, FINSEQ_1:def 7;
then ( ( ('not' H) . (1 + i) = x implies F . a = y ) & ('not' H) . (1 + i) = H . a & ( ('not' H) . (1 + i) <> x implies F . a = ('not' H) . (1 + i) ) ) by A1, A2, A3, A4, A5, A7, Def4, FINSEQ_1:def 7;
then ( ( H . a = x or H . a <> x ) & ( H . a = x implies (H / x,y) . a = y ) & ( H . a <> x implies (H / x,y) . a = H . a ) & ( H . a = x implies F . a = y ) & ( H . a <> x implies F . a = H . a ) ) by A2, A3, A5, A7, Def4;
hence F . a = (H / x,y) . a ; :: thesis: verum

end;

hence F = H / x,y by A6, FUNCT_1:9; :: thesis: verum

end;

assume A8: F = H / x,y ; :: thesis: 'not' F = ('not' H) / x,y
then A9: dom F = dom H by Def4;
then A10: len F = len H by FINSEQ_3:31;
then A11: ( dom ('not' F) = dom (('not' H) / x,y) & dom (('not' H) / x,y) = dom ('not' H) ) by A2, A3, Def4;

now

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

A13: now

assume i in {1} ; :: thesis: ('not' F) . a = (('not' H) / x,y) . a
then ( i = 1 & ('not' H) . 1 = 2 & 2 <> x ) by Th148, FINSEQ_1:58, TARSKI:def 1;
then ( ('not' F) . i = 2 & (('not' H) / x,y) . i = 2 ) by A2, A3, A10, A12, Def4, FINSEQ_1:58;
hence ('not' F) . a = (('not' H) / x,y) . a ; :: thesis: verum

end;

now

given j being Nat such that A14: ( j in dom F & i = 1 + j ) ; :: thesis: ('not' F) . a = (('not' H) / x,y) . a
( H . j = ('not' H) . i & F . j = ('not' F) . i ) by A1, A9, A14, FINSEQ_1:def 7;
then ( ( ('not' H) . a <> x implies ('not' F) . a = ('not' H) . a ) & ( ('not' H) . a = x implies ('not' F) . a = y ) & ( ('not' H) . a <> x implies (('not' H) / x,y) . a = ('not' H) . a ) & ( ('not' H) . a = x implies (('not' H) / x,y) . a = y ) ) by A2, A3, A8, A10, A12, A14, Def4;
hence ('not' F) . a = (('not' H) / x,y) . a ; :: thesis: verum

end;

hence ('not' F) . a = (('not' H) / x,y) . a by A1, A12, A13, FINSEQ_1:38; :: thesis: verum

end;

hence 'not' F = ('not' H) / x,y by A11, FUNCT_1:9; :: thesis: verum