proposition: Lemma iim_fun_set1_E f y: function f -> (Vfi1 f y) = Zo (source f) (fun x => y = Vf f x).
proof: Proof. move => ff; set_extens t. by move /(iim_fun_set1_P _ ff) => pa; apply /Zo_P. by move => /Zo_P pa; apply /(iim_fun_set1_P _ ff). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)