let K be Cardinal; :: thesis: for x being object holds Sum (x .--> K) = K
let x be object ; :: thesis: Sum (x .--> K) = K
thus Sum (x .--> K) = card (Union (x .--> [:K,{x}:])) by Th4
.= card [:K,{x}:] by Th7
.= card K by CARD_1:69
.= K ; :: thesis: verum