reconsider D = the carrier of (QuotientOrder A) as a_partition of the carrier of A by Th47;
D eqSumOf f is nonnegative-yielding by Th56;
hence eqSumOf f is nonnegative-yielding by Def15; :: thesis: verum