A1: ( dom (H / x,y) = dom H & ( for a being set st a in dom H holds
( ( H . a = x implies (H / x,y) . a = y ) & ( H . a <> x implies (H / x,y) . a = H . a ) ) ) ) by Def4;
dom H = Seg (len H) by FINSEQ_1:def 3;
then reconsider f = H / x,y as FinSequence by A1, FINSEQ_1:def 2;
rng f c= NAT

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in rng f or a in NAT )
assume a in rng f ; :: thesis: a in NAT
then consider b being set such that
A2: ( b in dom f & a = f . b ) by FUNCT_1:def 5;
( ( H . b = x or H . b <> x ) & rng H c= NAT & H . b in rng H ) by A1, A2, FINSEQ_1:def 4, FUNCT_1:def 5;
then ( a = y or ( a = H . b & H . b in NAT ) ) by A1, A2;
hence a in NAT ; :: thesis: verum

end;

then reconsider f = f as FinSequence of NAT by FINSEQ_1:def 4;
f in WFF by Th171;
hence H / x,y is ZF-formula by ZF_LANG:14; :: thesis: verum