let M, N be Cardinal; :: thesis: Sum (M --> N) = M *` N
thus Sum (M --> N) = card [:N,M:] by CARD_3:25
.= M *` N by Lm2 ; :: thesis: verum