let K be Cardinal; :: thesis: Sum ({} --> K) = 0
dom ({} --> K) = {} ;
then dom (disjoin ({} --> K)) = {} by Def3;
hence Sum ({} --> K) = 0 by CARD_1:47, RELAT_1:65, ZFMISC_1:2; :: thesis: verum