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;
(max- f) . x = max ((- (f . x)),0.) by A4, Def3;
then - 0. <= - (- (f . x)) by A2, XXREAL_0:def 10;
hence (max+ f) . x = f . x by A5, XXREAL_0:def 10; :: thesis: verum