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