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