A1: dom (H / (x,y)) = dom H 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;
A2: 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;
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
A3: b in dom f and
A4: a = f . b by FUNCT_1:def 3;
( rng H c= NAT & H . b in rng H ) by A1, A3, FINSEQ_1:def 4, FUNCT_1:def 3;
then ( a = y or ( a = H . b & H . b in NAT ) ) by A1, A2, A3, A4;
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:4; :: thesis: verum