[isabelle] Question about sets?



I have the following subgoal:

\<And> (n::nat) (f::nat=>'a) (x::'a).
 {y. \<exists> j < n . y = f j} x ==>
 \<exists> i < n . f i = x

I need to get the j where x = f j and then instantiate the i to that value. 
I am such a neophyte that I do not know how to do this. 
Any suggestions would be appreciated.


Tim 




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.