proposition: Lemma char_fun_surjective X f: function_prop f X C2 -> exists2 A, sub A X & char_fun A X = f.
proof: Proof. move => [fy <- ty]. set W := Zo (source f) (fun z => Vf f z = \1c). have WX: sub W (source f) by apply: Zo_S. exists W => //. symmetry;rewrite/char_fun;apply: function_exten => //; aw; trivial. apply: char_fun_f. move => s sX /=; case: (inc_or_not s W) => ws. rewrite (char_fun_V_a WX ws); exact: (Zo_hi ws). rewrite (char_fun_V_b WX (setC_i sX ws)). move: (Vf_target fy sX); rewrite ty. by case /set2_P => // f1; case: ws; apply/Zo_P. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)