for X being set
for f being Function holds Funcs ((Union (disjoin f)),X), product (Funcs (f,X)) are_equipotent