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;

f . x <= 0. by A2, A5, XXREAL_0:def 10;

hence (max- f) . x = - (f . x) by A6, XXREAL_0:def 10; :: thesis: verum

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;

f . x <= 0. by A2, A5, XXREAL_0:def 10;

hence (max- f) . x = - (f . x) by A6, XXREAL_0:def 10; :: thesis: verum