proposition: Lemma range_ex : forall f y : E, axioms f -> inc y (range f) -> ex (fun x : E => (inc x (domain f) & V x f = y)).
proof: Proof. ir. unfold range in H0. pose (Image.ex H0); nin e; xd. assert (axioms f). am. unfold axioms in H; xd. pose (H x H1). set (a := pr1 x) in *. set (b := pr2 x) in *. apply ex_intro with a. xd. unfold a in |- *; ap lem2; au. assert (x = pair a (V a f)). unfold a in |- *. ap lem1; au. rewrite <- H2. unfold b in |- *. rewrite H5. sy; ap pr2_pair. Qed.
imports: set_theory