[isabelle] THE-operator


i would like to prove the following:

  ( THE A. {a. f a = {c1, c2, c3}} = {a. f a = A}  )         =        {c1, c2, c3}  

It may well be a 1 line proof but unfortunately im unfamiliar with substitution on THE-operator).

Many thanks!

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