theorem Th16: :: TOPS_5:16

for X being non empty set
for i, f being object holds
( f in product ({i} --> X) iff ex x being Element of X st f = {i} --> x )