theorem :: FUNCT_6:53

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