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