let X be non empty set ; :: thesis: for f being PartFunc of X,REAL
for x being set st x in dom f holds
( ( (max+ f) . x = f . x or (max+ f) . x = 0 ) & ( (max- f) . x = - (f . x) or (max- f) . x = 0 ) )
let f be PartFunc of X,REAL; :: thesis: for x being set st x in dom f holds
( ( (max+ f) . x = f . x or (max+ f) . x = 0 ) & ( (max- f) . x = - (f . x) or (max- f) . x = 0 ) )
let x be set ; :: thesis: ( x in dom f implies ( ( (max+ f) . x = f . x or (max+ f) . x = 0 ) & ( (max- f) . x = - (f . x) or (max- f) . x = 0 ) ) )
assume A1: x in dom f ; :: thesis: ( ( (max+ f) . x = f . x or (max+ f) . x = 0 ) & ( (max- f) . x = - (f . x) or (max- f) . x = 0 ) )
then ( (max+ (R_EAL f)) . x = (R_EAL f) . x or (max+ (R_EAL f)) . x = 0. ) by MESFUNC2:18;
hence ( (max+ f) . x = f . x or (max+ f) . x = 0 ) by Th30; :: thesis: ( (max- f) . x = - (f . x) or (max- f) . x = 0 )
A2: ( max+ (R_EAL f) = max+ f & max- (R_EAL f) = max- f ) by Th30;
( (max- (R_EAL f)) . x = - ((R_EAL f) . x) or (max- (R_EAL f)) . x = 0. ) by A1, MESFUNC2:18;
hence ( (max- f) . x = - (f . x) or (max- f) . x = 0 ) by A2, SUPINF_2:2; :: thesis: verum