proposition: Lemma Exercise6_5b E F: (sub_functions E F) <=cc (\Po (product E F)).
proof: Proof. move: (card_bijection (graph_of_function_fb E F)). by rewrite /graph_of_function; aw => ->; apply: sub_smaller; apply: Zo_S. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)