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;

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

suppose 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 ( x in dom (max+ f) & x in dom (max- f) ) by Def2, Def3;
then ( (max+ f) . x = max (f . x),0. & (max- f) . x = max (- (f . x)),0. ) by Def2, Def3;
hence ( ( (max+ f) . x = f . x or (max+ f) . x = 0. ) & ( (max- f) . x = - (f . x) or (max- f) . x = 0. ) ) by XXREAL_0:16; :: 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 A1, FUNCT_1:def 4; :: thesis: verum

end;

end;