let C be non empty set ; :: thesis: for f being PartFunc of C,ExtREAL
for x being Element of C st x in dom f & (max+ f) . x = 0. holds
(max- f) . x = - (f . x)
let f be PartFunc of C,ExtREAL; :: thesis: for x being Element of C st x in dom f & (max+ f) . x = 0. holds
(max- f) . x = - (f . x)
let x be Element of C; :: 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)
A3: x in dom (max+ f) by A1, Def2;
A4: x in dom (max- f) by A1, Def3;
A5: (max+ f) . x = max ((f . x),0.) by A3, Def2;
A6: (max- f) . x = max ((- (f . x)),0.) by A4, Def3;
f . x <= 0. by A2, A5, XXREAL_0:def 10;
hence (max- f) . x = - (f . x) by A6, XXREAL_0:def 10; :: thesis: verum