theorem Th1: :: FUNCT_6:1

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