let K be Cardinal; :: thesis: for x being set holds Sum (x .--> K) = K
let x be set ; :: thesis: Sum (x .--> K) = K
thus Sum (x .--> K) = card (Union (x .--> [:K,{x}:])) by Th12
.= card [:K,{x}:] by Th16
.= card K by CARD_1:69
.= K by CARD_1:def 2 ; :: thesis: verum