per cases ( A is empty or not A is empty ) ;

suppose A is empty ; :: thesis: D eqSumOf f is finite-support

hence D eqSumOf f is finite-support ; :: thesis: verum

end;

suppose not A is empty ; :: thesis: D eqSumOf f is finite-support

then reconsider B = A as non empty set ;
reconsider E = D as non empty a_partition of B ;
reconsider F = f as finite-support Function of B,REAL ;
(proj E) .: (support f) is finite ;
then support (E eqSumOf F) is finite by Th64, FINSET_1:1;
hence D eqSumOf f is finite-support by PRE_POLY:def 8; :: thesis: verum

end;

end;