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 )
dom f = C by FUNCT_2:def 1;
then ( dom (max+ f) = C & dom (max- f) = C ) by RFUNCT_3:def 10, RFUNCT_3:def 11;
hence ( max+ f is total & max- f is total ) by PARTFUN1:def 4; :: thesis: verum