let X be non empty set ; :: thesis: for f being PartFunc of X,REAL holds abs f = (max+ f) + (max- f)
let f be PartFunc of X,REAL; :: thesis: abs f = (max+ f) + (max- f)
abs f = R_EAL (abs f) ;
then abs f = |.(R_EAL f).| by Th44;
then abs f = (max+ (R_EAL f)) + (max- (R_EAL f)) by MESFUNC2:24;
then abs f = (R_EAL (max+ f)) + (max- (R_EAL f)) by Th30;
then abs f = (R_EAL (max+ f)) + (R_EAL (max- f)) by Th30;
then abs f = R_EAL ((max+ f) + (max- f)) by Th23;
hence abs f = (max+ f) + (max- f) ; :: thesis: verum