(proj A) .: (support f) is finite
;

then support (eqSumOf f) is finite by Th63, FINSET_1:1;

hence eqSumOf f is finite-support by PRE_POLY:def 8; :: thesis: verum

then support (eqSumOf f) is finite by Th63, FINSET_1:1;

hence eqSumOf f is finite-support by PRE_POLY:def 8; :: thesis: verum