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 = - (f . x) holds
(max+ f) . x = 0
let f be PartFunc of X,REAL; :: thesis: for x being set st x in dom f & (max- f) . x = - (f . x) holds
(max+ f) . x = 0
let x be set ; :: thesis: ( x in dom f & (max- f) . x = - (f . x) implies (max+ f) . x = 0 )
assume that
A1: x in dom f and
A2: (max- f) . x = - (f . x) ; :: thesis: (max+ f) . x = 0
- (f . x) = (max- (R_EAL f)) . x by A2, Th30;
then - ((R_EAL f) . x) = (max- (R_EAL f)) . x by SUPINF_2:2;
then (max+ (R_EAL f)) . x = 0. by A1, MESFUNC2:21;
hence (max+ f) . x = 0 by Th30; :: thesis: verum