proposition: Lemma dirim_restr f s : fgraph f -> sub s (domain f) -> range (restr f s) = direct_image f s.
proof: Proof. move => Ha sd. have Hb: fgraph (restr f s) by fprops. have Hc: domain (restr f s) = s by aw. set_extens t. move=> /(range_gP Hb) [x xs ->]; apply/dirim_P; exists x; try ue. by rewrite Hc in xs; move: (sd _ xs) => xd; rewrite LgV//; apply:fdomain_pr1. move/dirim_P => [x xs /(pr2_V Ha)];aw => ->. by apply/(range_gP Hb); rewrite Hc; ex_tac; rewrite LgV. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)