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;