proposition: Lemma function_set_iff : forall (a : E) (f : E1) (u : E), inc u (function_set a f) <-> in_function_set a f u.
proof: Proof. ir. unfold iff in |- *; xd; ir. unfold function_set in H. ap Bounded.lem1. ap in_fs_bounded. am. unfold function_set in |- *. ap Bounded.lem2. ap in_fs_bounded. am. Qed.
imports: set_theory