for K being Cardinal holds Product ({} --> K) = 1 by Th10, CARD_1:30;