set X = { i where i is Element of NAT : x. i in rng finSub } ;
defpred S₁[ set , set ] means ex i being Element of NAT st
( i = $1 & $2 = x. i );
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 A3: a in NAT ; :: thesis: ex b being set st S₁[a,b]
reconsider i = a as Element of NAT by A3;
take b = x. i; :: thesis: S₁[a,b]
take i ; :: thesis: ( i = a & b = x. i )
thus ( i = a & b = x. i ) ; :: thesis: verum

end;

consider f being Function such that
A4: ( dom f = NAT & ( for a being set st a in NAT holds
S₁[a,f . a] ) ) from CLASSES1:sch 1(A2);
f is one-to-one

proof

let a1, a2 be set ; :: according to FUNCT_1:def 8 :: thesis: ( not a1 in dom f or not a2 in dom f or not f . a1 = f . a2 or a1 = a2 )
assume A5: ( a1 in dom f & a2 in dom f & f . a1 = f . a2 ) ; :: thesis: a1 = a2
consider i1 being Element of NAT such that
A6: ( i1 = a1 & f . a1 = x. i1 ) by A4, A5;
consider i2 being Element of NAT such that
A7: ( i2 = a2 & f . a2 = x. i2 ) by A4, A5;
thus a1 = a2 by A5, A6, A7, ZFMISC_1:33; :: thesis: verum

end;

then A8: f | { i where i is Element of NAT : x. i in rng finSub } is one-to-one by FUNCT_1:84;
rng (f | { i where i is Element of NAT : x. i in rng finSub } ) c= rng finSub

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 rng finSub } ) or b in rng finSub )
assume b in rng (f | { i where i is Element of NAT : x. i in rng finSub } ) ; :: thesis: b in rng finSub
then consider a being set such that
A9: ( a in dom (f | { i where i is Element of NAT : x. i in rng finSub } ) & b = (f | { i where i is Element of NAT : x. i in rng finSub } ) . a ) by FUNCT_1:def 5;
A10: b = f . a by A9, FUNCT_1:70;
A11: ( a in { i where i is Element of NAT : x. i in rng finSub } & a in dom f ) by A9, RELAT_1:86;
then consider i being Element of NAT such that
A12: ( i = a & b = x. i ) by A4, A10;
consider i being Element of NAT such that
A13: ( a = i & x. i in rng finSub ) by A11;
thus b in rng finSub by A12, A13; :: thesis: verum

end;

then rng (f | { i where i is Element of NAT : x. i in rng finSub } ) is finite ;
then A14: dom (f | { i where i is Element of NAT : x. i in rng finSub } ) is finite by A8, CARD_1:97;
{ i where i is Element of NAT : x. i in rng finSub } 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 rng finSub } or a in NAT )
assume a in { i where i is Element of NAT : x. i in rng finSub } ; :: thesis: a in NAT
then consider i being Element of NAT such that
A15: ( a = i & x. i in rng finSub ) ;
thus a in NAT by A15; :: thesis: verum

end;

then reconsider X = { i where i is Element of NAT : x. i in rng finSub } as Subset of NAT ;
for a being set holds
( a in dom (f | X) iff ( a in X & a in dom f ) ) by RELAT_1:86;
then dom (f | X) = X /\ NAT by A4, XBOOLE_0:def 4;
hence { i where i is Element of NAT : x. i in rng finSub } is finite Subset of NAT by A14, XBOOLE_1:28; :: thesis: verum