theorem Th73: :: CARD_3:74

for S being non empty functional set
for i being set st i in dom (product" S) holds
(product" S) . i = { (f . i) where f is Element of S : verum }