fact: Definition productb f:= Zo (\Po ((domain f) \times (unionb f))) (fun z => [/\ fgraph z, domain z = domain f & forall i, inc i (domain f) -> inc (Vg z i) (Vg f i)]).
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)