defpred S₁[ set , set ] means ex i being Element of NAT st
( i = $1 & $2 = x. i );
set X = { i where i is Element of NAT : x. i in Bound_Vars p } ;
A1: { i where i is Element of NAT : x. i in Bound_Vars p } c= NAT

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in { i where i is Element of NAT : x. i in Bound_Vars p } or a in NAT )
assume a in { i where i is Element of NAT : x. i in Bound_Vars p } ; :: thesis: a in NAT
then ex i being Element of NAT st
( a = i & x. i in Bound_Vars p ) ;
hence a in NAT ; :: thesis: verum

end;

A2: for a being set st a in NAT holds
ex b being set st S₁[a,b]

proof

let a be set ; :: thesis: ( a in NAT implies ex b being set st S₁[a,b] )
assume a in NAT ; :: thesis: ex b being set st S₁[a,b]
then reconsider i = a as Element of NAT ;
take x. i ; :: thesis: S₁[a, x. i]
take i ; :: thesis: ( i = a & x. i = x. i )
thus ( i = a & x. i = x. i ) ; :: thesis: verum

end;

consider f being Function such that
A3: ( dom f = NAT & ( for a being set st a in NAT holds
S₁[a,f . a] ) ) from CLASSES1:sch 1(A2);
A4: rng (f | { i where i is Element of NAT : x. i in Bound_Vars p } ) c= Bound_Vars p

proof

let b be set ; :: according to TARSKI:def 3 :: thesis: ( not b in rng (f | { i where i is Element of NAT : x. i in Bound_Vars p } ) or b in Bound_Vars p )
assume b in rng (f | { i where i is Element of NAT : x. i in Bound_Vars p } ) ; :: thesis: b in Bound_Vars p
then consider a being set such that
A5: a in dom (f | { i where i is Element of NAT : x. i in Bound_Vars p } ) and
A6: b = (f | { i where i is Element of NAT : x. i in Bound_Vars p } ) . a by FUNCT_1:def 3;
a in { i where i is Element of NAT : x. i in Bound_Vars p } by A5, RELAT_1:57;
then A7: ex i being Element of NAT st
( a = i & x. i in Bound_Vars p ) ;
( b = f . a & a in dom f ) by A5, A6, FUNCT_1:47, RELAT_1:57;
then ex i being Element of NAT st
( i = a & b = x. i ) by A3;
hence b in Bound_Vars p by A7; :: thesis: verum

end;

f is one-to-one

proof

let a1, a2 be set ; :: according to FUNCT_1:def 4 :: thesis: ( not a1 in proj1 f or not a2 in proj1 f or not f . a1 = f . a2 or a1 = a2 )
assume that
A8: ( a1 in dom f & a2 in dom f ) and
A9: f . a1 = f . a2 ; :: thesis: a1 = a2
( ex i1 being Element of NAT st
( i1 = a1 & f . a1 = x. i1 ) & ex i2 being Element of NAT st
( i2 = a2 & f . a2 = x. i2 ) ) by A3, A8;
hence a1 = a2 by A9, ZFMISC_1:27; :: thesis: verum

end;

then f | { i where i is Element of NAT : x. i in Bound_Vars p } is one-to-one by FUNCT_1:52;
then A10: dom (f | { i where i is Element of NAT : x. i in Bound_Vars p } ) is finite by A4, CARD_1:59;
reconsider X = { i where i is Element of NAT : x. i in Bound_Vars p } as Subset of NAT by A1;
for a being set holds
( a in dom (f | X) iff ( a in X & a in dom f ) ) by RELAT_1:57;
then dom (f | X) = X /\ NAT by A3, XBOOLE_0:def 4;
hence { i where i is Element of NAT : x. i in Bound_Vars p } is finite Subset of NAT by A10, XBOOLE_1:28; :: thesis: verum