theorem Th15: :: TOPS_5:15

for X being non empty set
for i being object holds product ({i} --> X) = { ({i} --> x) where x is Element of X : verum }