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 set such that
A1:
a in dom H
and
A2:
x = H . a
by FUNCT_1:def 5;
A3:
dom (H / x,y) = dom H
by Def4;
A4:
not y in {0 ,1,2,3,4}
by Th149;
(H / x,y) . a = y
by A1, A2, Def4;
then
y in rng (H / x,y)
by A1, A3, FUNCT_1:def 5;
hence
y in variables_in (H / x,y)
by A4, XBOOLE_0:def 5; verum