let H be ZF-formula; :: thesis: for x, y being Variable st H is negative holds
the_argument_of (H / x,y) = (the_argument_of H) / x,y
let x, y be Variable; :: thesis: ( H is negative implies the_argument_of (H / x,y) = (the_argument_of H) / x,y )
assume H is negative ; :: thesis: the_argument_of (H / x,y) = (the_argument_of H) / x,y
then ( H / x,y is negative & H = 'not' (the_argument_of H) ) by Th182, ZF_LANG:def 30;
then ( H / x,y = 'not' (the_argument_of (H / x,y)) & H / x,y = 'not' ((the_argument_of H) / x,y) ) by Th170, ZF_LANG:def 30;
hence the_argument_of (H / x,y) = (the_argument_of H) / x,y by FINSEQ_1:46; :: thesis: verum