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 ;
per cases ( x in dom f or not x in dom f ) ;
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 ;
A5: (max+ f) . x = max ((f . x),0.) by ;
(max- f) . x = max ((- (f . x)),0.) by ;
hence ( ( (max+ f) . x = f . x or (max+ f) . x = 0. ) & ( (max- f) . x = - (f . x) or (max- f) . x = 0. ) ) by ; :: thesis: verum
end;
suppose not 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. ) )
hence ( ( (max+ f) . x = f . x or (max+ f) . x = 0. ) & ( (max- f) . x = - (f . x) or (max- f) . x = 0. ) ) by ; :: thesis: verum
end;
end;