let C be non empty set ; :: thesis: for f being Function of C,REAL holds
( max+ f is total & max- f is total )
let f be Function of C,REAL; :: thesis: ( max+ f is total & max- f is total )
A1: dom f = C by FUNCT_2:def 1;
then A2: dom (max- f) = C by RFUNCT_3:def 11;
dom (max+ f) = C by A1, RFUNCT_3:def 10;
hence ( max+ f is total & max- f is total ) by A2, PARTFUN1:def 2; :: thesis: verum