theorem :: CARD_3:80

for f being non-empty Function
for p being Element of sproduct f ex s being Element of product f st p c= s