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: 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 A4: x in dom f ; :: thesis: |.f.| . x = ((max+ f) + (max- f)) . x

now

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

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

then A7: ((max+ f) . x) + ((max- f) . x) = (f . x) + 0. by Th21
.= f . x by XXREAL_3:4 ;
x in dom (max+ f) by A4, Def2;
then (max+ f) . x = max ((f . x),0.) by Def2;
then 0. <= f . x by A6, XXREAL_0:def 10;
then f . x = |.(f . x).| by EXTREAL1:def 3
.= |.f.| . x by A2, A4, MESFUNC1:def 10 ;
hence |.f.| . x = ((max+ f) + (max- f)) . x by A1, A4, A7, MESFUNC1:def 3; :: thesis: verum

end;

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

then A13: ((max+ f) . x) + ((max- f) . x) = 0. + (- (f . x)) by A4, Th22
.= - (f . x) by XXREAL_3:4 ;
x in dom (max+ f) by A4, Def2;
then (max+ f) . x = max ((f . x),0.) by Def2;
then f . x <= 0. by A12, XXREAL_0:def 10;
then - (f . x) = |.(f . x).| by EXTREAL2:55
.= |.f.| . x by A2, A4, MESFUNC1:def 10 ;
hence |.f.| . x = ((max+ f) + (max- f)) . x by A1, A4, A13, MESFUNC1:def 3; :: thesis: verum

end;

end;

end;

hence |.f.| . x = ((max+ f) + (max- f)) . x ; :: thesis: verum

end;

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