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

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;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