proposition: Lemma graph_of_function_fb x y: bijection (graph_of_function x y).
proof: Proof. rewrite /graph_of_function. apply: lf_bijective. by apply: set_of_graphs_pr. move=> u v /sfunctionsP [fu ssu tu] /sfunctionsP [fv sv tv] sg. by apply: function_exten1=>//; ue. move=> z /Zo_P [] /setP_P zp fx. have gz:= (sub_setX_graph zp). exists (triple (domain z) y z); last by aw. apply/sfunctionsP;saw. apply: function_pr => //. by move => t /(rangeP gz) [u Jz]; move: (zp _ Jz) => /setXp_P []. by move => t /(domainP gz) [u Jz]; move: (zp _ Jz) => /setXp_P []. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)