proposition: Lemma dirim_setn0 f u: sgraph f -> nonempty u -> sub u (domain f) -> nonempty (direct_image f u).
proof: Proof. move=> gr [x xu] udf; move: (udf _ xu); case /(domainP gr)=> [y Jr]. exists y;apply: Zo_i; ex_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)