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