theorem Th13: :: TOPS_5:13

for X, Y being non empty set
for y being Element of Y holds X --> y in product (X --> Y)