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:20;
then (max- f) . x = - ((R_EAL f) . x) by Th30;
hence (max- f) . x = - (f . x) by SUPINF_2:2; :: thesis: verum