let C be non empty set ; :: thesis: for f being PartFunc of C,ExtREAL

for x being Element of C st 0. < (max+ f) . x holds

(max- f) . x = 0.

let f be PartFunc of C,ExtREAL; :: thesis: for x being Element of C st 0. < (max+ f) . x holds

(max- f) . x = 0.

let x be Element of C; :: thesis: ( 0. < (max+ f) . x implies (max- f) . x = 0. )

A1: dom (max+ f) = dom f by Def2;

for x being Element of C st 0. < (max+ f) . x holds

(max- f) . x = 0.

let f be PartFunc of C,ExtREAL; :: thesis: for x being Element of C st 0. < (max+ f) . x holds

(max- f) . x = 0.

let x be Element of C; :: thesis: ( 0. < (max+ f) . x implies (max- f) . x = 0. )

A1: dom (max+ f) = dom f by Def2;

per cases
( x in dom f or not x in dom f )
;

end;

suppose A2:
x in dom f
; :: thesis: ( 0. < (max+ f) . x implies (max- f) . x = 0. )

assume A3:
0. < (max+ f) . x
; :: thesis: (max- f) . x = 0.

A4: x in dom (max+ f) by A2, Def2;

A5: x in dom (max- f) by A2, Def3;

(max+ f) . x = max ((f . x),0.) by A4, Def2;

then ( not f . x <= 0. or not 0. <= 0. ) by A3, XXREAL_0:28;

then max ((- (f . x)),0.) = 0. by XXREAL_0:def 10;

hence (max- f) . x = 0. by A5, Def3; :: thesis: verum

end;A4: x in dom (max+ f) by A2, Def2;

A5: x in dom (max- f) by A2, Def3;

(max+ f) . x = max ((f . x),0.) by A4, Def2;

then ( not f . x <= 0. or not 0. <= 0. ) by A3, XXREAL_0:28;

then max ((- (f . x)),0.) = 0. by XXREAL_0:def 10;

hence (max- f) . x = 0. by A5, Def3; :: thesis: verum