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