let K be Cardinal; :: thesis: for x being set holds Product (x .--> K) = K
let x be set ; :: thesis: Product (x .--> K) = K
thus Product (x .--> K) = card (Funcs ({x},K)) by Th20
.= card K by FUNCT_5:58
.= K by CARD_1:def 2 ; :: thesis: verum