proposition: Lemma Im_add : forall (X:Ensemble U) (x:U) (f:U -> V), Im (Add _ X x) f = Add _ (Im X f) (f x).
proof: Proof. intros X x f. apply Extensionality_Ensembles. split; red; intros x0 H'. - elim H'; intros. rewrite H0. elim Add_inv with U X x x1; auto using Im_def with sets. destruct 1; auto using Im_def with sets. - elim Add_inv with V (Im X f) (f x) x0. + destruct 1 as [x0 H y H0]. rewrite H0; auto using Im_def with sets. + destruct 1; auto using Im_def with sets. + trivial. Qed.
imports: Finite_sets Constructive_sets Classical Classical_sets Powerset Powerset_facts Powerset_Classical_facts Finite_sets_facts