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

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

hence
|.f.| = (max+ f) + (max- f)
by A1, A2, PARTFUN1:5; :: thesis: verum
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

end;assume A3: x in dom f ; :: thesis: |.f.| . x = ((max+ f) + (max- f)) . x

now :: thesis: |.f.| . x = ((max+ f) + (max- f)) . xend;

hence
|.f.| . x = ((max+ f) + (max- f)) . x
; :: thesis: verumper cases
( (max+ f) . x = f . x or (max+ f) . x = 0. )
by Th18;

end;

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 A3, Def2;

then (max+ f) . x = max ((f . x),0.) by Def2;

then 0. <= f . x by A4, XXREAL_0:def 10;

then f . x = |.(f . x).| by EXTREAL1:def 1

.= |.f.| . x by A2, A3, MESFUNC1:def 10 ;

hence |.f.| . x = ((max+ f) + (max- f)) . x by A1, A3, A5, MESFUNC1:def 3; :: thesis: verum

end;.= f . x by XXREAL_3:4 ;

x in dom (max+ f) by A3, Def2;

then (max+ f) . x = max ((f . x),0.) by Def2;

then 0. <= f . x by A4, XXREAL_0:def 10;

then f . x = |.(f . x).| by EXTREAL1:def 1

.= |.f.| . x by A2, A3, MESFUNC1:def 10 ;

hence |.f.| . x = ((max+ f) + (max- f)) . x by A1, A3, A5, MESFUNC1:def 3; :: thesis: verum

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 A3, Th20

.= - (f . x) by XXREAL_3:4 ;

x in dom (max+ f) by A3, Def2;

then (max+ f) . x = max ((f . x),0.) by Def2;

then f . x <= 0. by A6, XXREAL_0:def 10;

then - (f . x) = |.(f . x).| by EXTREAL1:18

.= |.f.| . x by A2, A3, MESFUNC1:def 10 ;

hence |.f.| . x = ((max+ f) + (max- f)) . x by A1, A3, A7, MESFUNC1:def 3; :: thesis: verum

end;.= - (f . x) by XXREAL_3:4 ;

x in dom (max+ f) by A3, Def2;

then (max+ f) . x = max ((f . x),0.) by Def2;

then f . x <= 0. by A6, XXREAL_0:def 10;

then - (f . x) = |.(f . x).| by EXTREAL1:18

.= |.f.| . x by A2, A3, MESFUNC1:def 10 ;

hence |.f.| . x = ((max+ f) + (max- f)) . x by A1, A3, A7, MESFUNC1:def 3; :: thesis: verum