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