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

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