let H be ZF-formula; for x, y being Variable st x in variables_in H holds
y in variables_in (H / (x,y))
let x, y be Variable; ( x in variables_in H implies y in variables_in (H / (x,y)) )
assume
x in variables_in H
; y in variables_in (H / (x,y))
then consider a being object such that
A1:
a in dom H
and
A2:
x = H . a
by FUNCT_1:def 3;
A3:
dom (H / (x,y)) = dom H
by Def3;
A4:
not y in {0,1,2,3,4}
by Th136;
(H / (x,y)) . a = y
by A1, A2, Def3;
then
y in rng (H / (x,y))
by A1, A3, FUNCT_1:def 3;
hence
y in variables_in (H / (x,y))
by A4, XBOOLE_0:def 5; verum