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