proposition: Lemma function_functional f: correspondence f -> (function f <-> (forall x, inc x (source f) -> exists! y, related (graph f) x y)).
proof: Proof. rewrite/related=> cf; split. move=> ff x xsf;exists (Vf f x); split; first by Wtac. move => y yg; symmetry; apply: (Vf_pr ff yg). move => eu. have sd:source f = domain (graph f). apply: extensionality; last by fprops. move=> t ts; move: (eu _ ts) => [y [ja jb]]. by apply/funI_P; ex_tac; aw. split=>//;apply /functionalP; split; first by fprops. move=> x y y'; rewrite /related => h1. have isf: inc x (source f) by rewrite sd; apply/funI_P; ex_tac; aw. move: h1; move/unique_existence: (eu _ isf) => [_]; apply. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)