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;
A2: dom f = dom |.f.| by MESFUNC1:def 10;
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
now :: thesis: |.f.| . x = ((max+ f) + (max- f)) . x
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 A5: ((max+ f) . x) + ((max- f) . x) = (f . x) + 0. by Th19
.= f . x by XXREAL_3:4 ;
x in dom (max+ f) by ;
then (max+ f) . x = max ((f . x),0.) by Def2;
then 0. <= f . x by ;
then f . x = |.(f . x).| by EXTREAL1:def 1
.= |.f.| . x by ;
hence |.f.| . x = ((max+ f) + (max- f)) . x by ; :: thesis: verum
end;
suppose A6: (max+ f) . x = 0. ; :: thesis: |.f.| . x = ((max+ f) + (max- f)) . x
then A7: ((max+ f) . x) + ((max- f) . x) = 0. + (- (f . x)) by
.= - (f . x) by XXREAL_3:4 ;
x in dom (max+ f) by ;
then (max+ f) . x = max ((f . x),0.) by Def2;
then f . x <= 0. by ;
then - (f . x) = |.(f . x).| by EXTREAL1:18
.= |.f.| . x by ;
hence |.f.| . x = ((max+ f) + (max- f)) . x by ; :: thesis: verum
end;
end;
end;
hence |.f.| . x = ((max+ f) + (max- f)) . x ; :: thesis: verum
end;
hence |.f.| = (max+ f) + (max- f) by ; :: thesis: verum