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 Th17;
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 A2: x in dom f ; :: thesis: f . x = ((max+ f) - (max- f)) . x
then A3: ((max+ f) - (max- f)) . x = ((max+ f) . x) - ((max- f) . x) by A1, MESFUNC1:def 4;

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

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

then (max- f) . x = 0. by Th19;
then - ((max- f) . x) = 0 ;
hence f . x = ((max+ f) - (max- f)) . x by A3, A4, XXREAL_3:4; :: thesis: verum

end;

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

then (max- f) . x = - (f . x) by A2, Th20;
hence f . x = ((max+ f) - (max- f)) . x by A3, A5, XXREAL_3:4; :: thesis: verum

end;

end;

end;

hence f = (max+ f) - (max- f) by A1, PARTFUN1:5; :: thesis: verum