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