proposition: Lemma finite_image : forall (X:Ensemble U) (f:U -> V), Finite _ X -> Finite _ (Im X f).
proof: Proof. intros X f H'; elim H'. - rewrite (image_empty f); auto with sets. - intros A H'0 H'1 x H'2; clear H' X. rewrite (Im_add A x f); auto with sets. apply Add_preserves_Finite; auto with sets. Qed.
imports: Finite_sets Constructive_sets Classical Classical_sets Powerset Powerset_facts Powerset_Classical_facts Finite_sets_facts