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