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 that
A1: x in dom f and
A2: (max- f) . x = 0 ; :: thesis: (max+ f) . x = f . x
0 = (max- (R_EAL f)) . x by A2, Th30;
then (max+ (R_EAL f)) . x = (R_EAL f) . x by A1, MESFUNC2:22;
hence (max+ f) . x = f . x by Th30; :: thesis: verum