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 ) ) )
A1: - ((R_EAL f) . x) = - (f . x) by SUPINF_2:3;
assume A2: 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:20;
hence ( (max+ f) . x = f . x or (max+ f) . x = 0 ) by Th30; :: thesis: ( (max- f) . x = - (f . x) or (max- f) . x = 0 )
( (max- (R_EAL f)) . x = - ((R_EAL f) . x) or (max- (R_EAL f)) . x = 0. ) by A2, MESFUNC2:20;
hence ( (max- f) . x = - (f . x) or (max- f) . x = 0 ) by A1, Th30; :: thesis: verum