let C be non empty set ; :: thesis: for f being PartFunc of C,ExtREAL
for x being Element of C st (max- f) . x = - (f . x) holds
(max+ f) . x = 0.
let f be PartFunc of C,ExtREAL ; :: thesis: for x being Element of C st (max- f) . x = - (f . x) holds
(max+ f) . x = 0.
let x be Element of C; :: thesis: ( (max- f) . x = - (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 ) ;

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

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

end;

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

thus ( (max- f) . x = - (f . x) implies (max+ f) . x = 0. ) by A1, A9, FUNCT_1:def 4; :: thesis: verum

end;

end;