proposition: Lemma dirim_domain f: sgraph f -> direct_image f (domain f) = range f.
proof: Proof. move=> sgf; apply: extensionality; first by apply: dirim_Sr. move => t /funI_P [y yf ->]; apply: Zo_i; first by fprops. by exists (P y); fprops;rewrite (sgf _ yf). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)