proposition: Lemma setX_range x y: nonempty x -> range (x \times y) = y.
proof: Proof. move=> [z zy]; set_extens t. by case/(funI_P) => u /setX_P [_ _ xx] ->. move=> tx; apply/funI_P;exists (J z t); aw; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)