proposition: Lemma function_rest_of_prolongation f g: extends g f -> f = restriction2 g (source f) (target f).
proof: Proof. move=>[ff fg]. move /(sub_functionP ff fg)=> [_ sts sg] st. have au: (sub (Vfs g (source f)) (target f)). by move =>t /(Vf_image_P fg sts) [u us ->]; rewrite - sg=>//; fprops. have ax: (restriction2_axioms g (source f) (target f)) by []. apply: function_exten;fprops; try solve [rewrite /restriction2; aw;trivial]. apply: (proj31 (restriction2_prop ax)). by move => x sf /=; rewrite restriction2_V // sg. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)