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;
A3: 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

A5: 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

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

end;

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

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

end;

end;

end;

thus |.f.| . x = ((max+ f) + (max- f)) . x by A5; :: thesis: verum

end;

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