for f being Function holds product f c= Funcs ((dom f),(Union f))