About Finite Set of records

Hi gang,

Given a set S, of records where each record has a field f such that \A s \in S: s[f] \in Nat, I am trying to prove the following lemma:

    IsFiniteSet(S) => IsFiniteSet({s.f: s \in S})

As far as I could tell, there is no direct theorem in FiniteSetTheorems which can discharge this. There however are other ways. Some of them are:

    1) Prove that {s.f: s \in S} can be obtained from a surjection on S and then use FS_Surjection.
    2) Prove that \A s \in S : IsFiniteSet({s.f}) using FS_Singleton and then use FS_UNION to prove {{s.f}: s \in S} is finite. But I think here the above surjection would still be needed.
    3) Write an inductive proof on S.

I was wondering if others have tried to prove something along the lines of this before (collection of elements of finite sets of records), and how have others tried to prove it.

Thanks,
Saksham Chand