proposition: Lemma restriction1_fs f x: function f -> sub x (source f) -> surjection (restriction1 f x).
proof: Proof. move=> ff sxs. have [pa pb pc] := (restriction1_prop ff sxs). split => //y; rewrite pb pc; move/(Vf_image_P ff sxs) => [b bx Jg]. by ex_tac; aw; rewrite restriction1_V. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)