reconsider D = the carrier of (QuotientOrder A) as a_partition of the carrier of A by Th47;
reconsider F = D eqSumOf f as Function of (QuotientOrder A),REAL ;
take F ; :: thesis: ex D being a_partition of the carrier of A st
( D = the carrier of (QuotientOrder A) & F = D eqSumOf f )
take D ; :: thesis: ( D = the carrier of (QuotientOrder A) & F = D eqSumOf f )
thus ( D = the carrier of (QuotientOrder A) & F = D eqSumOf f ) ; :: thesis: verum