[isabelle] One more theorem missing in ZF

It seems that the following theorem is also forgotten in ZF:
lemma fun_range_subset: "f: A->B ==> range(f) <= B" sorry
What is the best way to prove it? (Ideally I would like to see both apply-style and ISAR proofs.)
I started to maintain the theory ZF_Addons, a theory where lemmas forgotten in ZF would be stored until they will be added to the ZF core in a next release of Isabelle. (I plan to submit this to IsarMathLib.)
Victor Porton - http://portonvictor.org

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