let M, N be Cardinal; :: thesis: Sum (M --> N) = M *` N
thus Sum (M --> N) = card [:N,M:] by Th36
.= M *` N by CARD_2:def 2 ; :: thesis: verum