let C be non empty set ; :: thesis: for f being PartFunc of C,ExtREAL holds f = (max+ f) - (max- f)
let f be PartFunc of C,ExtREAL ; :: thesis: f = (max+ f) - (max- f)
A1: dom f = dom ((max+ f) - (max- f)) by Th19;
A2: for x being Element of C st x in dom f holds
f . x = ((max+ f) - (max- f)) . x

proof

let x be Element of C; :: thesis: ( x in dom f implies f . x = ((max+ f) - (max- f)) . x )
assume A3: x in dom f ; :: thesis: f . x = ((max+ f) - (max- f)) . x
A4: ((max+ f) - (max- f)) . x = ((max+ f) . x) - ((max- f) . x) by A1, A3, MESFUNC1:def 4;

per cases ( (max+ f) . x = f . x or (max+ f) . x = 0. ) by Th20;

suppose A5: (max+ f) . x = f . x ; :: thesis: f . x = ((max+ f) - (max- f)) . x

A6: (max- f) . x = 0. by A5, Th21;
A7: - ((max- f) . x) = 0 by A6;
thus f . x = ((max+ f) - (max- f)) . x by A4, A5, A7, XXREAL_3:4; :: thesis: verum

end;

suppose A8: (max+ f) . x = 0. ; :: thesis: f . x = ((max+ f) - (max- f)) . x

A9: (max- f) . x = - (f . x) by A3, A8, Th22;
thus f . x = ((max+ f) - (max- f)) . x by A4, A8, A9, XXREAL_3:4; :: thesis: verum

end;

end;

end;

thus f = (max+ f) - (max- f) by A1, A2, PARTFUN1:34; :: thesis: verum