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