let H be ZF-formula; :: thesis: for x, y being Variable st not x in variables_in H holds
H / (x,y) = H
let x, y be Variable; :: thesis: ( not x in variables_in H implies H / (x,y) = H )
assume A1: not x in variables_in H ; :: thesis: H / (x,y) = H
A2: not x in {0,1,2,3,4} by Th136;

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

let a be object ; :: thesis: ( a in dom H implies (H / (x,y)) . a = H . a )
assume A4: a in dom H ; :: thesis: (H / (x,y)) . a = H . a
then A5: H . a in rng H by FUNCT_1:def 3;
( H . a <> x implies (H / (x,y)) . a = H . a ) by A4, Def3;
hence (H / (x,y)) . a = H . a by A1, A2, A5, XBOOLE_0:def 5; :: thesis: verum

end;

dom H = dom (H / (x,y)) by Def3;
hence H / (x,y) = H by A3, FUNCT_1:2; :: thesis: verum