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

for x being Element of C holds

( ( (max+ f) . x = f . x or (max+ f) . x = 0. ) & ( (max- f) . x = - (f . x) or (max- f) . x = 0. ) )

let f be PartFunc of C,ExtREAL; :: thesis: for x being Element of C holds

( ( (max+ f) . x = f . x or (max+ f) . x = 0. ) & ( (max- f) . x = - (f . x) or (max- f) . x = 0. ) )

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

A1: ( dom (max- f) = dom f & dom (max+ f) = dom f ) by Def2, Def3;

for x being Element of C holds

( ( (max+ f) . x = f . x or (max+ f) . x = 0. ) & ( (max- f) . x = - (f . x) or (max- f) . x = 0. ) )

let f be PartFunc of C,ExtREAL; :: thesis: for x being Element of C holds

( ( (max+ f) . x = f . x or (max+ f) . x = 0. ) & ( (max- f) . x = - (f . x) or (max- f) . x = 0. ) )

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

A1: ( dom (max- f) = dom f & dom (max+ f) = dom f ) by Def2, Def3;

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

end;

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

then A3:
x in dom (max+ f)
by Def2;

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

A5: (max+ f) . x = max ((f . x),0.) by A3, Def2;

(max- f) . x = max ((- (f . x)),0.) by A4, Def3;

hence ( ( (max+ f) . x = f . x or (max+ f) . x = 0. ) & ( (max- f) . x = - (f . x) or (max- f) . x = 0. ) ) by A5, XXREAL_0:16; :: thesis: verum

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

A5: (max+ f) . x = max ((f . x),0.) by A3, Def2;

(max- f) . x = max ((- (f . x)),0.) by A4, Def3;

hence ( ( (max+ f) . x = f . x or (max+ f) . x = 0. ) & ( (max- f) . x = - (f . x) or (max- f) . x = 0. ) ) by A5, XXREAL_0:16; :: thesis: verum