(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