theorem Th60: :: CARD_3:60

for x, y being object
for f being Function st x in dom f & y in f . x holds
x .--> y in sproduct f