let C be non empty set ; 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; 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; ( 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.
; (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; verum