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;

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

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

hence (max+ f) . x = f . x by A5, 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;

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

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

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