let k, m be Element of NAT ; :: thesis: Sum (k --> m) = k * m
A1: ( (k --> m) " {m} = k & card k = k ) by CARD_1:def 5, FUNCOP_1:21;
( rng (k --> m) c= {m} & {m} c= {0 ,m} ) by FUNCOP_1:19, ZFMISC_1:12;
hence Sum (k --> m) = k * m by A1, CARD_FIN:45, XBOOLE_1:1; :: thesis: verum