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