proposition: Lemma function_set_inc : forall (a : E) (f : E1) (u : E), Function.axioms u -> Function.domain u = a -> (forall y : E, inc y a -> inc (V y u) (f y)) -> inc u (function_set a f).
proof: Proof. ir. pose (function_set_iff a f u). unfold iff in (type of i); xd. ap H3. unfold in_function_set in |- *; xd. Qed.
imports: set_theory