mesfun6c.miz



    begin

    theorem :: MESFUN6C:1

    for a,b be Real holds (a + b) = (a + b) & ( - a) = ( - a) & (a - b) = (a - b) & (a * b) = (a * b);

    begin

    reserve X for non empty set,

Y for set,

S for SigmaField of X,

M for sigma_Measure of S,

f,g for PartFunc of X, COMPLEX ,

r for Real,

c for Complex,

E,A,B for Element of S;

    definition

      let X be non empty set;

      let S be SigmaField of X;

      let E be Element of S;

      let f be PartFunc of X, COMPLEX ;

      :: MESFUN6C:def1

      attr f is E -measurable means ( Re f) is E -measurable & ( Im f) is E -measurable;

    end

    theorem :: MESFUN6C:2

    

     Th2: (r (#) ( Re f)) = ( Re (r (#) f)) & (r (#) ( Im f)) = ( Im (r (#) f))

    proof

      

       A1: ( dom (r (#) ( Re f))) = ( dom ( Re f)) by VALUED_1:def 5;

      

       A3: ( Im r) = 0 by COMPLEX1:def 2;

      

       A4: ( dom ( Re f)) = ( dom f) by COMSEQ_3:def 3;

      

       A5: ( Re r) = r by COMPLEX1:def 1;

      

       A6: ( dom (r (#) f)) = ( dom f) by VALUED_1:def 5;

      

       A7: ( dom ( Re (r (#) f))) = ( dom (r (#) f)) by COMSEQ_3:def 3;

      now

        let x be object;

        

         A8: ( Re (r * (f . x))) = ((( Re r) * ( Re (f . x))) - (( Im r) * ( Im (f . x)))) by COMPLEX1: 9;

        assume

         A9: x in ( dom (r (#) ( Re f)));

        then

         A10: (( Re f) . x) = ( Re (f . x)) by A1, COMSEQ_3:def 3;

        (( Re (r (#) f)) . x) = ( Re ((r (#) f) . x)) by A1, A6, A7, A4, A9, COMSEQ_3:def 3;

        then (( Re (r (#) f)) . x) = (r * ( Re (f . x))) by A1, A6, A4, A5, A3, A9, A8, VALUED_1:def 5;

        hence ((r (#) ( Re f)) . x) = (( Re (r (#) f)) . x) by A9, A10, VALUED_1:def 5;

      end;

      hence (r (#) ( Re f)) = ( Re (r (#) f)) by A1, A6, A7, A4, FUNCT_1: 2;

      

       A11: ( dom (r (#) ( Im f))) = ( dom ( Im f)) by VALUED_1:def 5;

      

       A12: ( dom ( Im f)) = ( dom f) by COMSEQ_3:def 4;

      

       A13: ( dom ( Im (r (#) f))) = ( dom (r (#) f)) by COMSEQ_3:def 4;

      now

        let x be object;

        

         A14: ( Im (r * (f . x))) = ((( Im r) * ( Re (f . x))) + (( Re r) * ( Im (f . x)))) by COMPLEX1: 9;

        assume

         A15: x in ( dom (r (#) ( Im f)));

        then

         A16: (( Im f) . x) = ( Im (f . x)) by A11, COMSEQ_3:def 4;

        (( Im (r (#) f)) . x) = ( Im ((r (#) f) . x)) by A11, A6, A13, A12, A15, COMSEQ_3:def 4;

        then (( Im (r (#) f)) . x) = (r * ( Im (f . x))) by A11, A6, A12, A5, A3, A15, A14, VALUED_1:def 5;

        hence ((r (#) ( Im f)) . x) = (( Im (r (#) f)) . x) by A15, A16, VALUED_1:def 5;

      end;

      hence thesis by A11, A6, A13, A12, FUNCT_1: 2;

    end;

    theorem :: MESFUN6C:3

    

     Th3: ( Re (c (#) f)) = ((( Re c) (#) ( Re f)) - (( Im c) (#) ( Im f))) & ( Im (c (#) f)) = ((( Im c) (#) ( Re f)) + (( Re c) (#) ( Im f)))

    proof

      

       A1: ( dom (( Re c) (#) ( Re f))) = ( dom ( Re f)) by VALUED_1:def 5;

      

       A2: ( dom (( Im c) (#) ( Im f))) = ( dom ( Im f)) by VALUED_1:def 5;

      

       A3: ( dom (c (#) f)) = ( dom f) by VALUED_1:def 5;

      

       A4: ( dom ( Re (c (#) f))) = ( dom (c (#) f)) by COMSEQ_3:def 3;

      

       A5: ( dom ( Re f)) = ( dom f) by COMSEQ_3:def 3;

      

       A6: ( dom ( Im f)) = ( dom f) by COMSEQ_3:def 4;

      

       A7: ( dom ((( Re c) (#) ( Re f)) - (( Im c) (#) ( Im f)))) = (( dom (( Re c) (#) ( Re f))) /\ ( dom (( Im c) (#) ( Im f)))) by VALUED_1: 12;

      now

        let x be object;

        

         A8: ( Re (c * (f . x))) = ((( Re c) * ( Re (f . x))) - (( Im c) * ( Im (f . x)))) by COMPLEX1: 9;

        assume

         A9: x in ( dom ( Re (c (#) f)));

        then

         A10: ((( Im c) (#) ( Im f)) . x) = (( Im c) * (( Im f) . x)) by A4, A6, A2, A3, VALUED_1:def 5;

        

         A11: (( Im f) . x) = ( Im (f . x)) by A4, A6, A3, A9, COMSEQ_3:def 4;

        

         A12: (( Re f) . x) = ( Re (f . x)) by A4, A5, A3, A9, COMSEQ_3:def 3;

        (( Re (c (#) f)) . x) = ( Re ((c (#) f) . x)) by A9, COMSEQ_3:def 3;

        then

         A13: (( Re (c (#) f)) . x) = ( Re (c * (f . x))) by A4, A9, VALUED_1:def 5;

        ((( Re c) (#) ( Re f)) . x) = (( Re c) * (( Re f) . x)) by A4, A5, A1, A3, A9, VALUED_1:def 5;

        hence (( Re (c (#) f)) . x) = (((( Re c) (#) ( Re f)) - (( Im c) (#) ( Im f))) . x) by A4, A5, A6, A1, A2, A3, A7, A9, A13, A10, A12, A11, A8, VALUED_1: 13;

      end;

      hence ( Re (c (#) f)) = ((( Re c) (#) ( Re f)) - (( Im c) (#) ( Im f))) by A4, A5, A6, A1, A2, A3, A7, FUNCT_1: 2;

      

       A14: ( dom (( Im c) (#) ( Re f))) = ( dom ( Re f)) by VALUED_1:def 5;

      

       A15: ( dom (( Re c) (#) ( Im f))) = ( dom ( Im f)) by VALUED_1:def 5;

      

       A16: ( dom ( Im (c (#) f))) = ( dom (c (#) f)) by COMSEQ_3:def 4;

      

       A17: ( dom ((( Im c) (#) ( Re f)) + (( Re c) (#) ( Im f)))) = (( dom (( Im c) (#) ( Re f))) /\ ( dom (( Re c) (#) ( Im f)))) by VALUED_1:def 1;

      now

        let x be object;

        assume

         A18: x in ( dom ( Im (c (#) f)));

        then

         A19: ((( Im c) (#) ( Re f)) . x) = (( Im c) * (( Re f) . x)) by A5, A16, A14, A3, VALUED_1:def 5;

        (( Im (c (#) f)) . x) = ( Im ((c (#) f) . x)) by A18, COMSEQ_3:def 4;

        then

         A20: (( Im (c (#) f)) . x) = ( Im (c * (f . x))) by A16, A18, VALUED_1:def 5;

        

         A21: (( Im f) . x) = ( Im (f . x)) by A16, A6, A3, A18, COMSEQ_3:def 4;

        

         A22: (( Re f) . x) = ( Re (f . x)) by A5, A16, A3, A18, COMSEQ_3:def 3;

        

         A23: ((( Re c) (#) ( Im f)) . x) = (( Re c) * (( Im f) . x)) by A16, A6, A15, A3, A18, VALUED_1:def 5;

        (((( Im c) (#) ( Re f)) + (( Re c) (#) ( Im f))) . x) = (((( Im c) (#) ( Re f)) . x) + ((( Re c) (#) ( Im f)) . x)) by A5, A16, A6, A14, A15, A3, A17, A18, VALUED_1:def 1;

        hence (( Im (c (#) f)) . x) = (((( Im c) (#) ( Re f)) + (( Re c) (#) ( Im f))) . x) by A20, A19, A23, A22, A21, COMPLEX1: 9;

      end;

      hence thesis by A5, A16, A6, A14, A15, A3, A17, FUNCT_1: 2;

    end;

    theorem :: MESFUN6C:4

    

     Th4: ( - ( Im f)) = ( Re ( <i> (#) f)) & ( Re f) = ( Im ( <i> (#) f))

    proof

      

       A1: ( dom ( - ( Im f))) = ( dom ( Im f)) by VALUED_1: 8;

      

       A2: ( dom ( <i> (#) f)) = ( dom f) by VALUED_1:def 5;

      

       A3: ( dom ( Im f)) = ( dom f) by COMSEQ_3:def 4;

      

       A4: ( dom ( Re ( <i> (#) f))) = ( dom ( <i> (#) f)) by COMSEQ_3:def 3;

      now

        let x be object;

        

         A5: (( - ( Im f)) . x) = ( - (( Im f) . x)) by VALUED_1: 8;

        

         A6: ( Re ( <i> * (f . x))) = ((( Re <i> ) * ( Re (f . x))) - (( Im <i> ) * ( Im (f . x)))) by COMPLEX1: 9;

        assume

         A7: x in ( dom ( - ( Im f)));

        then (( Re ( <i> (#) f)) . x) = ( Re (( <i> (#) f) . x)) by A1, A4, A2, A3, COMSEQ_3:def 3;

        then (( Re ( <i> (#) f)) . x) = ( - ( Im (f . x))) by A1, A2, A3, A7, A6, COMPLEX1: 7, VALUED_1:def 5;

        hence (( - ( Im f)) . x) = (( Re ( <i> (#) f)) . x) by A1, A7, A5, COMSEQ_3:def 4;

      end;

      hence ( - ( Im f)) = ( Re ( <i> (#) f)) by A4, A2, A3, FUNCT_1: 2, VALUED_1: 8;

      

       A8: ( dom ( Re f)) = ( dom f) by COMSEQ_3:def 3;

      

       A9: ( dom ( Im ( <i> (#) f))) = ( dom ( <i> (#) f)) by COMSEQ_3:def 4;

      now

        let x be object;

        

         A10: ( Im ( <i> * (f . x))) = ((( Im <i> ) * ( Re (f . x))) + (( Re <i> ) * ( Im (f . x)))) by COMPLEX1: 9;

        assume

         A11: x in ( dom ( Re f));

        then (( Im ( <i> (#) f)) . x) = ( Im (( <i> (#) f) . x)) by A8, A2, A9, COMSEQ_3:def 4;

        then (( Im ( <i> (#) f)) . x) = ( Re (f . x)) by A8, A2, A11, A10, COMPLEX1: 7, VALUED_1:def 5;

        hence (( Re f) . x) = (( Im ( <i> (#) f)) . x) by A11, COMSEQ_3:def 3;

      end;

      hence thesis by A8, A2, A9, FUNCT_1: 2;

    end;

    theorem :: MESFUN6C:5

    

     Th5: ( Re (f + g)) = (( Re f) + ( Re g)) & ( Im (f + g)) = (( Im f) + ( Im g))

    proof

      

       A1: ( dom ( Re (f + g))) = ( dom (f + g)) by COMSEQ_3:def 3;

      

       A2: ( dom ( Re g)) = ( dom g) by COMSEQ_3:def 3;

      

       A3: ( dom ( Re f)) = ( dom f) by COMSEQ_3:def 3;

      then ( dom (( Re f) + ( Re g))) = (( dom f) /\ ( dom g)) by A2, VALUED_1:def 1;

      then

       A4: ( dom ( Re (f + g))) = ( dom (( Re f) + ( Re g))) by A1, VALUED_1:def 1;

      now

        let x be object;

        assume

         A5: x in ( dom ( Re (f + g)));

        then (( Re (f + g)) . x) = ( Re ((f + g) . x)) by COMSEQ_3:def 3;

        then (( Re (f + g)) . x) = ( Re ((f . x) + (g . x))) by A1, A5, VALUED_1:def 1;

        then

         A6: (( Re (f + g)) . x) = (( Re (f . x)) + ( Re (g . x))) by COMPLEX1: 8;

        

         A7: x in (( dom f) /\ ( dom g)) by A1, A5, VALUED_1:def 1;

        then x in ( dom ( Re g)) by A2, XBOOLE_0:def 4;

        then

         A8: (( Re g) . x) = ( Re (g . x)) by COMSEQ_3:def 3;

        x in ( dom ( Re f)) by A3, A7, XBOOLE_0:def 4;

        then (( Re f) . x) = ( Re (f . x)) by COMSEQ_3:def 3;

        hence (( Re (f + g)) . x) = ((( Re f) + ( Re g)) . x) by A4, A5, A6, A8, VALUED_1:def 1;

      end;

      hence ( Re (f + g)) = (( Re f) + ( Re g)) by A4, FUNCT_1: 2;

      

       A9: ( dom ( Im (f + g))) = ( dom (f + g)) by COMSEQ_3:def 4;

      

       A10: ( dom ( Im g)) = ( dom g) by COMSEQ_3:def 4;

      

       A11: ( dom ( Im f)) = ( dom f) by COMSEQ_3:def 4;

      then ( dom (( Im f) + ( Im g))) = (( dom f) /\ ( dom g)) by A10, VALUED_1:def 1;

      then

       A12: ( dom ( Im (f + g))) = ( dom (( Im f) + ( Im g))) by A9, VALUED_1:def 1;

      now

        let x be object;

        assume

         A13: x in ( dom ( Im (f + g)));

        then (( Im (f + g)) . x) = ( Im ((f + g) . x)) by COMSEQ_3:def 4;

        then (( Im (f + g)) . x) = ( Im ((f . x) + (g . x))) by A9, A13, VALUED_1:def 1;

        then

         A14: (( Im (f + g)) . x) = (( Im (f . x)) + ( Im (g . x))) by COMPLEX1: 8;

        

         A15: x in (( dom f) /\ ( dom g)) by A9, A13, VALUED_1:def 1;

        then x in ( dom ( Im g)) by A10, XBOOLE_0:def 4;

        then

         A16: (( Im g) . x) = ( Im (g . x)) by COMSEQ_3:def 4;

        x in ( dom ( Im f)) by A11, A15, XBOOLE_0:def 4;

        then (( Im f) . x) = ( Im (f . x)) by COMSEQ_3:def 4;

        hence (( Im (f + g)) . x) = ((( Im f) + ( Im g)) . x) by A12, A13, A14, A16, VALUED_1:def 1;

      end;

      hence thesis by A12, FUNCT_1: 2;

    end;

    theorem :: MESFUN6C:6

    

     Th6: ( Re (f - g)) = (( Re f) - ( Re g)) & ( Im (f - g)) = (( Im f) - ( Im g))

    proof

      ( Re (f - g)) = (( Re f) + ( Re ( - g))) by Th5;

      then

       A1: ( Re (f - g)) = (( Re f) + (( - 1) (#) ( Re g))) by Th2;

      ( Im (f - g)) = (( Im f) + ( Im ( - g))) by Th5;

      hence thesis by A1, Th2;

    end;

    theorem :: MESFUN6C:7

    

     Th7: (( Re f) | A) = ( Re (f | A)) & (( Im f) | A) = ( Im (f | A))

    proof

      ( dom (( Re f) | A)) = (( dom ( Re f)) /\ A) by RELAT_1: 61

      .= (( dom f) /\ A) by COMSEQ_3:def 3;

      

      then

       A1: ( dom (( Re f) | A)) = ( dom (f | A)) by RELAT_1: 61

      .= ( dom ( Re (f | A))) by COMSEQ_3:def 3;

      now

        let x be object;

        assume

         A2: x in ( dom (( Re f) | A));

        then

         A3: x in (( dom ( Re f)) /\ A) by RELAT_1: 61;

        then

         A4: x in ( dom ( Re f)) by XBOOLE_0:def 4;

        

         A5: x in A by A3, XBOOLE_0:def 4;

        

        thus (( Re (f | A)) . x) = ( Re ((f | A) . x)) by A1, A2, COMSEQ_3:def 3

        .= ( Re (f . x)) by A5, FUNCT_1: 49

        .= (( Re f) . x) by A4, COMSEQ_3:def 3

        .= ((( Re f) | A) . x) by A5, FUNCT_1: 49;

      end;

      hence (( Re f) | A) = ( Re (f | A)) by A1, FUNCT_1: 2;

      ( dom (( Im f) | A)) = (( dom ( Im f)) /\ A) by RELAT_1: 61

      .= (( dom f) /\ A) by COMSEQ_3:def 4;

      

      then

       A6: ( dom (( Im f) | A)) = ( dom (f | A)) by RELAT_1: 61

      .= ( dom ( Im (f | A))) by COMSEQ_3:def 4;

      now

        let x be object;

        assume

         A7: x in ( dom (( Im f) | A));

        then

         A8: x in (( dom ( Im f)) /\ A) by RELAT_1: 61;

        then

         A9: x in ( dom ( Im f)) by XBOOLE_0:def 4;

        

         A10: x in A by A8, XBOOLE_0:def 4;

        

        thus (( Im (f | A)) . x) = ( Im ((f | A) . x)) by A6, A7, COMSEQ_3:def 4

        .= ( Im (f . x)) by A10, FUNCT_1: 49

        .= (( Im f) . x) by A9, COMSEQ_3:def 4

        .= ((( Im f) | A) . x) by A10, FUNCT_1: 49;

      end;

      hence thesis by A6, FUNCT_1: 2;

    end;

    theorem :: MESFUN6C:8

    

     Th8: f = (( Re f) + ( <i> (#) ( Im f)))

    proof

      

       A1: ( dom f) = ( dom ( Re f)) by COMSEQ_3:def 3;

      

       A2: ( dom f) = ( dom ( Im f)) by COMSEQ_3:def 4;

      

       A3: ( dom (( Re f) + ( <i> (#) ( Im f)))) = (( dom ( Re f)) /\ ( dom ( <i> (#) ( Im f)))) by VALUED_1:def 1

      .= (( dom f) /\ ( dom f)) by A1, A2, VALUED_1:def 5;

      

       A4: ( dom ( <i> (#) ( Im f))) = ( dom ( Im f)) by VALUED_1:def 5;

      now

        let x be object;

        assume

         A5: x in ( dom (( Re f) + ( <i> (#) ( Im f))));

        

        then ((( Re f) + ( <i> (#) ( Im f))) . x) = ((( Re f) . x) + (( <i> (#) ( Im f)) . x)) by VALUED_1:def 1

        .= (( Re (f . x)) + (( <i> (#) ( Im f)) . x)) by A1, A3, A5, COMSEQ_3:def 3

        .= (( Re (f . x)) + ( <i> * (( Im f) . x))) by A2, A4, A3, A5, VALUED_1:def 5

        .= (( Re (f . x)) + ( <i> * ( Im (f . x)))) by A2, A3, A5, COMSEQ_3:def 4;

        hence ((( Re f) + ( <i> (#) ( Im f))) . x) = (f . x) by COMPLEX1: 13;

      end;

      hence thesis by A3, FUNCT_1: 2;

    end;

    theorem :: MESFUN6C:9

    B c= A & f is A -measurable implies f is B -measurable by MESFUNC6: 16;

    theorem :: MESFUN6C:10

    f is A -measurable & f is B -measurable implies f is (A \/ B) -measurable by MESFUNC6: 17;

    theorem :: MESFUN6C:11

    f is A -measurable & g is A -measurable implies (f + g) is A -measurable

    proof

      assume that

       A1: f is A -measurable and

       A2: g is A -measurable;

      

       A3: ( Im g) is A -measurable by A2;

      ( Im f) is A -measurable by A1;

      then (( Im f) + ( Im g)) is A -measurable by A3, MESFUNC6: 26;

      then

       A4: ( Im (f + g)) is A -measurable by Th5;

      

       A5: ( Re g) is A -measurable by A2;

      ( Re f) is A -measurable by A1;

      then (( Re f) + ( Re g)) is A -measurable by A5, MESFUNC6: 26;

      then ( Re (f + g)) is A -measurable by Th5;

      hence thesis by A4;

    end;

    theorem :: MESFUN6C:12

    f is A -measurable & g is A -measurable & A c= ( dom g) implies (f - g) is A -measurable

    proof

      assume that

       A1: f is A -measurable and

       A2: g is A -measurable and

       A3: A c= ( dom g);

      

       A4: ( Im g) is A -measurable by A2;

      

       A5: A c= ( dom ( Re g)) by A3, COMSEQ_3:def 3;

      

       A6: ( Re g) is A -measurable by A2;

      

       A7: A c= ( dom ( Im g)) by A3, COMSEQ_3:def 4;

      ( Im f) is A -measurable by A1;

      then (( Im f) - ( Im g)) is A -measurable by A4, A7, MESFUNC6: 29;

      then

       A8: ( Im (f - g)) is A -measurable by Th6;

      ( Re f) is A -measurable by A1;

      then (( Re f) - ( Re g)) is A -measurable by A6, A5, MESFUNC6: 29;

      then ( Re (f - g)) is A -measurable by Th6;

      hence thesis by A8;

    end;

    theorem :: MESFUN6C:13

    Y c= ( dom (f + g)) implies ( dom ((f | Y) + (g | Y))) = Y & ((f + g) | Y) = ((f | Y) + (g | Y))

    proof

      

       A1: ( dom (f + g)) = (( dom f) /\ ( dom g)) by VALUED_1:def 1;

      assume

       A2: Y c= ( dom (f + g));

      then

       A3: ( dom ((f + g) | Y)) = Y by RELAT_1: 62;

      ( dom (g | Y)) = (( dom g) /\ Y) by RELAT_1: 61;

      then

       A4: ( dom (g | Y)) = Y by A2, A1, XBOOLE_1: 18, XBOOLE_1: 28;

      ( dom (f | Y)) = (( dom f) /\ Y) by RELAT_1: 61;

      then

       A5: ( dom (f | Y)) = Y by A2, A1, XBOOLE_1: 18, XBOOLE_1: 28;

      then

       A6: ( dom ((f | Y) + (g | Y))) = (Y /\ Y) by A4, VALUED_1:def 1;

      now

        let x be object;

        assume

         A7: x in ( dom ((f + g) | Y));

        

        hence (((f + g) | Y) . x) = ((f + g) . x) by FUNCT_1: 47

        .= ((f . x) + (g . x)) by A2, A3, A7, VALUED_1:def 1

        .= (((f | Y) . x) + (g . x)) by A3, A5, A7, FUNCT_1: 47

        .= (((f | Y) . x) + ((g | Y) . x)) by A3, A4, A7, FUNCT_1: 47

        .= (((f | Y) + (g | Y)) . x) by A3, A6, A7, VALUED_1:def 1;

      end;

      hence thesis by A2, A6, FUNCT_1: 2, RELAT_1: 62;

    end;

    theorem :: MESFUN6C:14

    f is B -measurable & A = (( dom f) /\ B) implies (f | B) is A -measurable

    proof

      assume that

       A1: f is B -measurable and

       A2: A = (( dom f) /\ B);

      

       A3: A = (( dom ( Im f)) /\ B) by A2, COMSEQ_3:def 4;

      ( Im f) is B -measurable by A1;

      then (( Im f) | B) is A -measurable by A3, MESFUNC6: 76;

      then

       A4: ( Im (f | B)) is A -measurable by Th7;

      

       A5: A = (( dom ( Re f)) /\ B) by A2, COMSEQ_3:def 3;

      ( Re f) is B -measurable by A1;

      then (( Re f) | B) is A -measurable by A5, MESFUNC6: 76;

      then ( Re (f | B)) is A -measurable by Th7;

      hence thesis by A4;

    end;

    theorem :: MESFUN6C:15

    ( dom f) in S & ( dom g) in S implies ( dom (f + g)) in S

    proof

      assume that

       A1: ( dom f) in S and

       A2: ( dom g) in S;

      reconsider E1 = ( dom f), E2 = ( dom g) as Element of S by A1, A2;

      ( dom (f + g)) = (E1 /\ E2) by VALUED_1:def 1;

      hence thesis;

    end;

    theorem :: MESFUN6C:16

    ( dom f) = A implies (f is B -measurable iff f is (A /\ B) -measurable)

    proof

      assume

       A1: ( dom f) = A;

      then

       A2: ( dom ( Re f)) = A by COMSEQ_3:def 3;

      

       A3: ( dom ( Im f)) = A by A1, COMSEQ_3:def 4;

      hence f is B -measurable implies f is (A /\ B) -measurable by A2, MESFUNC6: 80;

      thus thesis by A2, A3, MESFUNC6: 80;

    end;

    theorem :: MESFUN6C:17

    

     Th17: f is A -measurable & A c= ( dom f) implies (c (#) f) is A -measurable

    proof

      assume that

       A1: f is A -measurable and

       A2: A c= ( dom f);

      

       A3: ( dom ( Im f)) = ( dom f) by COMSEQ_3:def 4;

      

       A4: ( Im f) is A -measurable by A1;

      then

       A5: (( Re c) (#) ( Im f)) is A -measurable by A2, A3, MESFUNC6: 21;

      

       A6: (( Im c) (#) ( Im f)) is A -measurable by A2, A4, A3, MESFUNC6: 21;

      

       A7: ( dom ( Re f)) = ( dom f) by COMSEQ_3:def 3;

      

       A8: ( Re f) is A -measurable by A1;

      then (( Im c) (#) ( Re f)) is A -measurable by A2, A7, MESFUNC6: 21;

      then ((( Im c) (#) ( Re f)) + (( Re c) (#) ( Im f))) is A -measurable by A5, MESFUNC6: 26;

      then

       A9: ( Im (c (#) f)) is A -measurable by Th3;

      ( dom (( Im c) (#) ( Im f))) = ( dom ( Im f)) by VALUED_1:def 5;

      then

       A10: A c= ( dom (( Im c) (#) ( Im f))) by A2, COMSEQ_3:def 4;

      (( Re c) (#) ( Re f)) is A -measurable by A2, A8, A7, MESFUNC6: 21;

      then ((( Re c) (#) ( Re f)) - (( Im c) (#) ( Im f))) is A -measurable by A6, A10, MESFUNC6: 29;

      then ( Re (c (#) f)) is A -measurable by Th3;

      hence thesis by A9;

    end;

    theorem :: MESFUN6C:18

    (ex A be Element of S st ( dom f) = A) implies for c be Complex, B be Element of S st f is B -measurable holds (c (#) f) is B -measurable

    proof

      assume ex A be Element of S st A = ( dom f);

      then

      consider A be Element of S such that

       A1: A = ( dom f);

      hereby

        let c be Complex, B be Element of S;

        

         A2: ( dom (( Re c) (#) ( Re f))) = ( dom ( Re f)) by VALUED_1:def 5;

        

         A3: ( dom (( Im c) (#) ( Im f))) = ( dom ( Im f)) by VALUED_1:def 5;

        ( dom ( Re (c (#) f))) = ( dom ((( Re c) (#) ( Re f)) - (( Im c) (#) ( Im f)))) by Th3;

        then

         A4: ( dom ( Re (c (#) f))) = (( dom (( Re c) (#) ( Re f))) /\ ( dom (( Im c) (#) ( Im f)))) by VALUED_1: 12;

        

         A5: ( dom (( Im c) (#) ( Re f))) = ( dom ( Re f)) by VALUED_1:def 5;

        ( dom ( Im (c (#) f))) = ( dom ((( Im c) (#) ( Re f)) + (( Re c) (#) ( Im f)))) by Th3;

        then

         A6: ( dom ( Im (c (#) f))) = (( dom (( Im c) (#) ( Re f))) /\ ( dom (( Re c) (#) ( Im f)))) by VALUED_1:def 1;

        

         A7: ( dom (( Re c) (#) ( Im f))) = ( dom ( Im f)) by VALUED_1:def 5;

        

         A8: ( dom ( Re f)) = ( dom f) by COMSEQ_3:def 3;

        

         A9: ( dom ( Im f)) = ( dom f) by COMSEQ_3:def 4;

        assume

         A10: f is B -measurable;

        then ( Im f) is B -measurable;

        then

         A11: ( Im f) is (A /\ B) -measurable by A1, A9, MESFUNC6: 80;

        ( Re f) is B -measurable by A10;

        then ( Re f) is (A /\ B) -measurable by A1, A8, MESFUNC6: 80;

        then f is (A /\ B) -measurable by A11;

        then

         A12: (c (#) f) is (A /\ B) -measurable by A1, Th17, XBOOLE_1: 17;

        then ( Im (c (#) f)) is (A /\ B) -measurable;

        then

         A13: ( Im (c (#) f)) is B -measurable by A1, A8, A9, A5, A7, A6, MESFUNC6: 80;

        ( Re (c (#) f)) is (A /\ B) -measurable by A12;

        then ( Re (c (#) f)) is B -measurable by A1, A8, A9, A2, A3, A4, MESFUNC6: 80;

        hence (c (#) f) is B -measurable by A13;

      end;

    end;

    begin

    definition

      let X be non empty set;

      let S be SigmaField of X;

      let M be sigma_Measure of S;

      let f be PartFunc of X, COMPLEX ;

      :: MESFUN6C:def2

      pred f is_integrable_on M means ( Re f) is_integrable_on M & ( Im f) is_integrable_on M;

    end

    definition

      let X be non empty set;

      let S be SigmaField of X;

      let M be sigma_Measure of S;

      let f be PartFunc of X, COMPLEX ;

      assume

       A1: f is_integrable_on M;

      :: MESFUN6C:def3

      func Integral (M,f) -> Complex means

      : Def3: ex R,I be Real st R = ( Integral (M,( Re f))) & I = ( Integral (M,( Im f))) & it = (R + (I * <i> ));

      existence

      proof

        

         A2: ( Im f) is_integrable_on M by A1;

        then

         A3: -infty < ( Integral (M,( Im f))) by MESFUNC6: 90;

        

         A4: ( Re f) is_integrable_on M by A1;

        then

         A5: ( Integral (M,( Re f))) < +infty by MESFUNC6: 90;

        

         A6: ( Integral (M,( Im f))) < +infty by A2, MESFUNC6: 90;

         -infty < ( Integral (M,( Re f))) by A4, MESFUNC6: 90;

        then

        reconsider R = ( Integral (M,( Re f))), I = ( Integral (M,( Im f))) as Element of REAL by A5, A3, A6, XXREAL_0: 14;

        take (R + (I * <i> ));

        thus thesis;

      end;

      uniqueness ;

    end

    

     Lm1: for X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f be PartFunc of X, ExtREAL holds ( max+ f) is nonnegative & ( max- f) is nonnegative

    proof

      let X be non empty set;

      let S be SigmaField of X;

      let M be sigma_Measure of S;

      let f be PartFunc of X, ExtREAL ;

      

       A1: for x be object st x in ( dom ( max- f)) holds 0 <= (( max- f) . x) by MESFUNC2: 13;

      for x be object st x in ( dom ( max+ f)) holds 0 <= (( max+ f) . x) by MESFUNC2: 12;

      hence thesis by A1, SUPINF_2: 52;

    end;

    theorem :: MESFUN6C:19

    

     Th19: for X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f be PartFunc of X, ExtREAL , A be Element of S st (ex E be Element of S st E = ( dom f) & f is E -measurable) & (M . A) = 0 holds (f | A) is_integrable_on M

    proof

      let X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f be PartFunc of X, ExtREAL , A be Element of S;

      assume that

       A1: ex E be Element of S st E = ( dom f) & f is E -measurable and

       A2: (M . A) = 0 ;

      

       A3: ( dom f) = ( dom ( max+ f)) by MESFUNC2:def 2;

      ( max+ f) is nonnegative by Lm1;

      then ( integral+ (M,(( max+ f) | A))) = 0 by A1, A2, A3, MESFUNC2: 25, MESFUNC5: 82;

      then

       A4: ( integral+ (M,( max+ (f | A)))) < +infty by MESFUNC5: 28;

      consider E be Element of S such that

       A5: E = ( dom f) and

       A6: f is E -measurable by A1;

      

       A7: (( dom f) /\ (A /\ E)) = (A /\ E) by A5, XBOOLE_1: 17, XBOOLE_1: 28;

      

       A8: ( dom f) = ( dom ( max- f)) by MESFUNC2:def 3;

      ( max- f) is nonnegative by Lm1;

      then ( integral+ (M,(( max- f) | A))) = 0 by A1, A2, A8, MESFUNC2: 26, MESFUNC5: 82;

      then

       A9: ( integral+ (M,( max- (f | A)))) < +infty by MESFUNC5: 28;

      

       A10: ( dom (f | A)) = (( dom f) /\ A) by RELAT_1: 61;

      f is (A /\ E) -measurable by A6, MESFUNC1: 30, XBOOLE_1: 17;

      then

       A11: (f | (A /\ E)) is (A /\ E) -measurable by A7, MESFUNC5: 42;

      (f | (A /\ E)) = ((f | A) /\ (f | E)) by RELAT_1: 79

      .= ((f | A) /\ f) by A5

      .= (f | A) by RELAT_1: 59, XBOOLE_1: 28;

      hence thesis by A5, A11, A10, A4, A9;

    end;

    theorem :: MESFUN6C:20

    

     Th20: for X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f be PartFunc of X, REAL , E,A be Element of S st (ex E be Element of S st E = ( dom f) & f is E -measurable) & (M . A) = 0 holds (f | A) is_integrable_on M by Th19;

    theorem :: MESFUN6C:21

    (ex E be Element of S st E = ( dom f) & f is E -measurable) & (M . A) = 0 implies (f | A) is_integrable_on M & ( Integral (M,(f | A))) = 0

    proof

      set g = (f | A);

      assume that

       A1: ex E be Element of S st E = ( dom f) & f is E -measurable and

       A2: (M . A) = 0 ;

      consider E be Element of S such that

       A3: E = ( dom f) and

       A4: f is E -measurable by A1;

      

       A5: ( dom ( Im f)) = ( dom f) by COMSEQ_3:def 4;

      

       A6: ( Im f) is E -measurable by A4;

      then

       A7: ( Integral (M,(( Im f) | A))) = 0 by A2, A3, A5, MESFUNC6: 88;

      (( Im f) | A) is_integrable_on M by A2, A3, A6, A5, Th20;

      then

       A8: ( Im g) is_integrable_on M by Th7;

      

       A9: ( dom ( Re f)) = ( dom f) by COMSEQ_3:def 3;

      

       A10: ( Im g) = (( Im f) | A) by Th7;

      

       A11: ( Re f) is E -measurable by A4;

      

       A12: ( Re g) = (( Re f) | A) by Th7;

      then

      reconsider R = ( Integral (M,( Re g))), I = ( Integral (M,( Im g))) as Real by A2, A3, A11, A6, A9, A5, A10, MESFUNC6: 88;

      (( Re f) | A) is_integrable_on M by A2, A3, A11, A9, Th20;

      then ( Re g) is_integrable_on M by Th7;

      hence g is_integrable_on M by A8;

      

      hence ( Integral (M,g)) = (R + (I * <i> )) by Def3

      .= 0 by A2, A3, A11, A9, A7, A12, A10, MESFUNC6: 88;

    end;

    theorem :: MESFUN6C:22

    E = ( dom f) & f is_integrable_on M & (M . A) = 0 implies ( Integral (M,(f | (E \ A)))) = ( Integral (M,f))

    proof

      assume that

       A1: E = ( dom f) and

       A2: f is_integrable_on M and

       A3: (M . A) = 0 ;

      set C = (E \ A);

      

       A4: ( dom f) = ( dom ( Re f)) by COMSEQ_3:def 3;

      

       A5: ( Im f) is_integrable_on M by A2;

      then ( R_EAL ( Im f)) is_integrable_on M;

      then

      consider IE be Element of S such that

       A6: IE = ( dom ( R_EAL ( Im f))) and

       A7: ( R_EAL ( Im f)) is IE -measurable;

      

       A8: ( dom f) = ( dom ( Im f)) by COMSEQ_3:def 4;

      

       A9: ( Integral (M,(( Im f) | C))) = ( Integral (M,( Im (f | C)))) by Th7;

      ( Im f) is IE -measurable by A7;

      then

       A10: ( Integral (M,( Im (f | C)))) = ( Integral (M,( Im f))) by A1, A3, A8, A6, A9, MESFUNC6: 89;

      (( Im f) | C) is_integrable_on M by A5, MESFUNC6: 91;

      then

       A11: ( Im (f | C)) is_integrable_on M by Th7;

      then

       A12: -infty < ( Integral (M,( Im (f | C)))) by MESFUNC6: 90;

      

       A13: ( Re f) is_integrable_on M by A2;

      then ( R_EAL ( Re f)) is_integrable_on M;

      then

      consider RE be Element of S such that

       A14: RE = ( dom ( R_EAL ( Re f))) and

       A15: ( R_EAL ( Re f)) is RE -measurable;

      

       A16: ( Integral (M,(( Re f) | C))) = ( Integral (M,( Re (f | C)))) by Th7;

      ( Re f) is RE -measurable by A15;

      then

       A17: ( Integral (M,( Re (f | C)))) = ( Integral (M,( Re f))) by A1, A3, A4, A14, A16, MESFUNC6: 89;

      (( Re f) | C) is_integrable_on M by A13, MESFUNC6: 91;

      then

       A18: ( Re (f | C)) is_integrable_on M by Th7;

      then

       A19: ( Integral (M,( Re (f | C)))) < +infty by MESFUNC6: 90;

      

       A20: ( Integral (M,( Im (f | C)))) < +infty by A11, MESFUNC6: 90;

       -infty < ( Integral (M,( Re (f | C)))) by A18, MESFUNC6: 90;

      then

      reconsider R2 = ( Integral (M,( Re (f | C)))), I2 = ( Integral (M,( Im (f | C)))) as Element of REAL by A19, A12, A20, XXREAL_0: 14;

      (f | (E \ A)) is_integrable_on M by A18, A11;

      

      hence ( Integral (M,(f | (E \ A)))) = (R2 + (I2 * <i> )) by Def3

      .= ( Integral (M,f)) by A2, A17, A10, Def3;

    end;

    theorem :: MESFUN6C:23

    

     Th23: f is_integrable_on M implies (f | A) is_integrable_on M

    proof

      assume

       A1: f is_integrable_on M;

      then ( Im f) is_integrable_on M;

      then (( Im f) | A) is_integrable_on M by MESFUNC6: 91;

      then

       A2: ( Im (f | A)) is_integrable_on M by Th7;

      ( Re f) is_integrable_on M by A1;

      then (( Re f) | A) is_integrable_on M by MESFUNC6: 91;

      then ( Re (f | A)) is_integrable_on M by Th7;

      hence thesis by A2;

    end;

    theorem :: MESFUN6C:24

    f is_integrable_on M & A misses B implies ( Integral (M,(f | (A \/ B)))) = (( Integral (M,(f | A))) + ( Integral (M,(f | B))))

    proof

      assume that

       A1: f is_integrable_on M and

       A2: A misses B;

      

       A3: (f | B) is_integrable_on M by A1, Th23;

      then

       A4: ( Re (f | B)) is_integrable_on M;

      then

       A5: ( Integral (M,( Re (f | B)))) < +infty by MESFUNC6: 90;

      

       A6: ( Im (f | B)) is_integrable_on M by A3;

      then

       A7: -infty < ( Integral (M,( Im (f | B)))) by MESFUNC6: 90;

      

       A8: ( Integral (M,( Im (f | B)))) < +infty by A6, MESFUNC6: 90;

       -infty < ( Integral (M,( Re (f | B)))) by A4, MESFUNC6: 90;

      then

      reconsider R2 = ( Integral (M,( Re (f | B)))), I2 = ( Integral (M,( Im (f | B)))) as Element of REAL by A5, A7, A8, XXREAL_0: 14;

      

       A9: (f | A) is_integrable_on M by A1, Th23;

      then

       A10: ( Re (f | A)) is_integrable_on M;

      then

       A11: ( Integral (M,( Re (f | A)))) < +infty by MESFUNC6: 90;

      set C = (A \/ B);

      

       A12: (f | (A \/ B)) is_integrable_on M by A1, Th23;

      then

       A13: ( Re (f | C)) is_integrable_on M;

      then

       A14: ( Integral (M,( Re (f | C)))) < +infty by MESFUNC6: 90;

      

       A15: ( Im (f | C)) is_integrable_on M by A12;

      then

       A16: -infty < ( Integral (M,( Im (f | C)))) by MESFUNC6: 90;

      

       A17: ( Integral (M,( Im (f | C)))) < +infty by A15, MESFUNC6: 90;

       -infty < ( Integral (M,( Re (f | C)))) by A13, MESFUNC6: 90;

      then

      reconsider R3 = ( Integral (M,( Re (f | C)))), I3 = ( Integral (M,( Im (f | C)))) as Element of REAL by A14, A16, A17, XXREAL_0: 14;

      

       A18: ( Integral (M,(f | (A \/ B)))) = (R3 + (I3 * <i> )) by A12, Def3;

      

       A19: ( Im (f | A)) is_integrable_on M by A9;

      then

       A20: -infty < ( Integral (M,( Im (f | A)))) by MESFUNC6: 90;

      

       A21: ( Integral (M,( Im (f | A)))) < +infty by A19, MESFUNC6: 90;

       -infty < ( Integral (M,( Re (f | A)))) by A10, MESFUNC6: 90;

      then

      reconsider R1 = ( Integral (M,( Re (f | A)))), I1 = ( Integral (M,( Im (f | A)))) as Element of REAL by A11, A20, A21, XXREAL_0: 14;

      ( Im f) is_integrable_on M by A1;

      then ( Integral (M,(( Im f) | (A \/ B)))) = (( Integral (M,(( Im f) | A))) + ( Integral (M,(( Im f) | B)))) by A2, MESFUNC6: 92;

      

      then ( Integral (M,(( Im f) | C))) = (( Integral (M,( Im (f | A)))) + ( Integral (M,(( Im f) | B)))) by Th7

      .= (( Integral (M,( Im (f | A)))) + ( Integral (M,( Im (f | B))))) by Th7;

      then I3 = (I1 + I2 qua ExtReal) by Th7;

      then

       A22: I3 = (I1 + I2);

      ( Re f) is_integrable_on M by A1;

      then ( Integral (M,(( Re f) | (A \/ B)))) = (( Integral (M,(( Re f) | A))) + ( Integral (M,(( Re f) | B)))) by A2, MESFUNC6: 92;

      

      then ( Integral (M,(( Re f) | C))) = (( Integral (M,( Re (f | A)))) + ( Integral (M,(( Re f) | B)))) by Th7

      .= (( Integral (M,( Re (f | A)))) + ( Integral (M,( Re (f | B))))) by Th7;

      then R3 = (R1 + R2 qua ExtReal) by Th7;

      then R3 = (R1 + R2);

      then ( Integral (M,(f | (A \/ B)))) = ((R1 + (I1 * <i> )) + (R2 + (I2 * <i> ))) by A22, A18;

      then ( Integral (M,(f | (A \/ B)))) = (( Integral (M,(f | A))) + (R2 + (I2 * <i> ))) by A9, Def3;

      hence thesis by A3, Def3;

    end;

    theorem :: MESFUN6C:25

    f is_integrable_on M & B = (( dom f) \ A) implies (f | A) is_integrable_on M & ( Integral (M,f)) = (( Integral (M,(f | A))) + ( Integral (M,(f | B))))

    proof

      assume that

       A1: f is_integrable_on M and

       A2: B = (( dom f) \ A);

      

       A3: ( Re f) is_integrable_on M by A1;

      then

       A4: ( Integral (M,( Re f))) < +infty by MESFUNC6: 90;

      

       A5: ( Im f) is_integrable_on M by A1;

      then

       A6: -infty < ( Integral (M,( Im f))) by MESFUNC6: 90;

      

       A7: ( Integral (M,( Im f))) < +infty by A5, MESFUNC6: 90;

       -infty < ( Integral (M,( Re f))) by A3, MESFUNC6: 90;

      then

      reconsider R = ( Integral (M,( Re f))), I = ( Integral (M,( Im f))) as Element of REAL by A4, A6, A7, XXREAL_0: 14;

      

       A8: ( Integral (M,f)) = (R + (I * <i> )) by A1, Def3;

      

       A9: (f | B) is_integrable_on M by A1, Th23;

      then

       A10: ( Re (f | B)) is_integrable_on M;

      then

       A11: ( Integral (M,( Re (f | B)))) < +infty by MESFUNC6: 90;

      

       A12: ( Im (f | B)) is_integrable_on M by A9;

      then

       A13: -infty < ( Integral (M,( Im (f | B)))) by MESFUNC6: 90;

      

       A14: ( Integral (M,( Im (f | B)))) < +infty by A12, MESFUNC6: 90;

       -infty < ( Integral (M,( Re (f | B)))) by A10, MESFUNC6: 90;

      then

      reconsider R2 = ( Integral (M,( Re (f | B)))), I2 = ( Integral (M,( Im (f | B)))) as Element of REAL by A11, A13, A14, XXREAL_0: 14;

      

       A15: (f | A) is_integrable_on M by A1, Th23;

      then

       A16: ( Re (f | A)) is_integrable_on M;

      then

       A17: ( Integral (M,( Re (f | A)))) < +infty by MESFUNC6: 90;

      

       A18: ( Im (f | A)) is_integrable_on M by A15;

      then

       A19: -infty < ( Integral (M,( Im (f | A)))) by MESFUNC6: 90;

      

       A20: ( Integral (M,( Im (f | A)))) < +infty by A18, MESFUNC6: 90;

       -infty < ( Integral (M,( Re (f | A)))) by A16, MESFUNC6: 90;

      then

      reconsider R1 = ( Integral (M,( Re (f | A)))), I1 = ( Integral (M,( Im (f | A)))) as Element of REAL by A17, A19, A20, XXREAL_0: 14;

      ( dom f) = ( dom ( Im f)) by COMSEQ_3:def 4;

      then ( Integral (M,( Im f))) = (( Integral (M,(( Im f) | A))) + ( Integral (M,(( Im f) | B)))) by A2, A5, MESFUNC6: 93;

      

      then ( Integral (M,( Im f))) = (( Integral (M,( Im (f | A)))) + ( Integral (M,(( Im f) | B)))) by Th7

      .= (( Integral (M,( Im (f | A)))) + ( Integral (M,( Im (f | B))))) by Th7;

      then

       A21: I = (I1 + I2) by SUPINF_2: 1;

      ( dom f) = ( dom ( Re f)) by COMSEQ_3:def 3;

      then ( Integral (M,( Re f))) = (( Integral (M,(( Re f) | A))) + ( Integral (M,(( Re f) | B)))) by A2, A3, MESFUNC6: 93;

      

      then ( Integral (M,( Re f))) = (( Integral (M,( Re (f | A)))) + ( Integral (M,(( Re f) | B)))) by Th7

      .= (( Integral (M,( Re (f | A)))) + ( Integral (M,( Re (f | B))))) by Th7;

      then R = (R1 + R2) by SUPINF_2: 1;

      then ( Integral (M,f)) = ((R1 + (I1 * <i> )) + (R2 + (I2 * <i> ))) by A21, A8;

      then ( Integral (M,f)) = (( Integral (M,(f | A))) + (R2 + (I2 * <i> ))) by A15, Def3;

      hence thesis by A1, A9, Def3, Th23;

    end;

    definition

      let k be Real, X be non empty set, f be PartFunc of X, REAL ;

      :: MESFUN6C:def4

      func f to_power k -> PartFunc of X, REAL means

      : Def4: ( dom it ) = ( dom f) & for x be Element of X st x in ( dom it ) holds (it . x) = ((f . x) to_power k);

      existence

      proof

        defpred P[ set, set] means $1 in ( dom f) & $2 = ((f . $1) to_power k);

        consider F be PartFunc of X, REAL such that

         A1: for z be Element of X holds z in ( dom F) iff ex c be Element of REAL st P[z, c] and

         A2: for z be Element of X st z in ( dom F) holds P[z, (F . z)] from SEQ_1:sch 2;

        take F;

        now

          let z be Element of X;

          hereby

            

             A3: ((f . z) to_power k) is Element of REAL by XREAL_0:def 1;

            assume z in ( dom f);

            hence z in ( dom F) by A1, A3;

          end;

          hereby

            assume z in ( dom F);

            then ex c be Element of REAL st P[z, c] by A1;

            hence z in ( dom f);

          end;

        end;

        hence ( dom F) = ( dom f) by SUBSET_1: 3;

        thus thesis by A2;

      end;

      uniqueness

      proof

        deffunc f0( set) = ((f . $1) to_power k);

        thus for h,g be PartFunc of X, REAL st (( dom h) = ( dom f) & for z be Element of X st z in ( dom h) holds (h . z) = f0(z)) & (( dom g) = ( dom f) & for z be Element of X st z in ( dom g) holds (g . z) = f0(z)) holds h = g from SEQ_1:sch 4;

      end;

    end

    registration

      let X;

      cluster nonnegative for PartFunc of X, REAL ;

      existence

      proof

        reconsider f = {} as Function;

        reconsider f as PartFunc of X, REAL by RELSET_1: 12;

        take f;

        let x be ExtReal;

        thus thesis;

      end;

    end

    registration

      let k be non negative Real, X;

      let f be nonnegative PartFunc of X, REAL ;

      cluster (f to_power k) -> nonnegative;

      coherence

      proof

        now

          let x be object;

          assume

           A1: x in ( dom (f to_power k));

          per cases ;

            suppose k = 0 ;

            then ((f . x) to_power k) = 1 by POWER: 24;

            hence 0 <= ((f to_power k) . x) by A1, Def4;

          end;

            suppose

             A2: k > 0 ;

            per cases by MESFUNC6: 51;

              suppose 0 < (f . x);

              then 0 < ((f . x) to_power k) by POWER: 34;

              hence 0 <= ((f to_power k) . x) by A1, Def4;

            end;

              suppose 0 = (f . x);

              then 0 = ((f . x) to_power k) by A2, POWER:def 2;

              hence 0 <= ((f to_power k) . x) by A1, Def4;

            end;

          end;

        end;

        hence thesis by MESFUNC6: 52;

      end;

    end

    theorem :: MESFUN6C:26

    

     Th26: for k be Real, X, S, E holds for f be PartFunc of X, REAL st f is nonnegative & 0 <= k holds (f to_power k) is nonnegative;

    theorem :: MESFUN6C:27

    

     Th27: for x be object, X, S, E holds for f be PartFunc of X, REAL st f is nonnegative holds ((f . x) to_power (1 / 2)) = ( sqrt (f . x))

    proof

      let x be object, X, S, E;

      let f be PartFunc of X, REAL ;

      assume f is nonnegative;

      then

       A1: 0 <= (f . x) by MESFUNC6: 51;

      

      hence ((f . x) to_power (1 / 2)) = (2 -root (f . x)) by POWER: 45

      .= (2 -Root (f . x)) by A1, POWER:def 1

      .= ( sqrt (f . x)) by A1, PREPOWER: 32;

    end;

    theorem :: MESFUN6C:28

    

     Th28: for f be PartFunc of X, REAL , a be Real st A c= ( dom f) holds (A /\ ( less_dom (f,a))) = (A \ (A /\ ( great_eq_dom (f,a))))

    proof

      let f be PartFunc of X, REAL , a be Real;

      now

        let x be object;

        assume

         A1: x in (A /\ ( less_dom (f,a)));

        then x in ( less_dom (f,a)) by XBOOLE_0:def 4;

        then ex y be Real st y = (f . x) & y < a by MESFUNC6: 3;

        then not (ex y1 be Real st y1 = (f . x) & a <= y1);

        then not x in ( great_eq_dom (f,a)) by MESFUNC6: 6;

        then

         A2: not x in (A /\ ( great_eq_dom (f,a))) by XBOOLE_0:def 4;

        x in A by A1, XBOOLE_0:def 4;

        hence x in (A \ (A /\ ( great_eq_dom (f,a)))) by A2, XBOOLE_0:def 5;

      end;

      then

       A3: (A /\ ( less_dom (f,a))) c= (A \ (A /\ ( great_eq_dom (f,a)))) by TARSKI:def 3;

      assume

       A4: A c= ( dom f);

      now

        let x be object;

        assume

         A5: x in (A \ (A /\ ( great_eq_dom (f,a))));

        then

         A6: x in A by XBOOLE_0:def 5;

         not x in (A /\ ( great_eq_dom (f,a))) by A5, XBOOLE_0:def 5;

        then not x in ( great_eq_dom (f,a)) by A6, XBOOLE_0:def 4;

        then not a <= (f . x) by A4, A6, MESFUNC6: 6;

        then x in ( less_dom (f,a)) by A4, A6, MESFUNC6: 3;

        hence x in (A /\ ( less_dom (f,a))) by A6, XBOOLE_0:def 4;

      end;

      then (A \ (A /\ ( great_eq_dom (f,a)))) c= (A /\ ( less_dom (f,a))) by TARSKI:def 3;

      hence thesis by A3, XBOOLE_0:def 10;

    end;

    reconsider jj = 1 as Real;

    theorem :: MESFUN6C:29

    

     Th29: for k be Real, X, S, E holds for f be PartFunc of X, REAL st f is nonnegative & 0 <= k & E c= ( dom f) & f is E -measurable holds (f to_power k) is E -measurable

    proof

      let k be Real, X, S, E;

      let f be PartFunc of X, REAL ;

      reconsider k1 = k as Real;

      assume that

       A1: f is nonnegative and

       A2: 0 <= k and

       A3: E c= ( dom f) and

       A4: f is E -measurable;

      

       A5: ( dom (f to_power k)) = ( dom f) by Def4;

      per cases by A2;

        suppose

         A6: k = 0 ;

        

         A7: E c= ( dom (f to_power k)) by A3, Def4;

        now

          let r be Real;

          reconsider r1 = r as Real;

          per cases ;

            suppose

             A8: r <= 1;

            now

              let x be object;

              assume

               A9: x in E;

              then ((f to_power k) . x) = ((f . x) to_power k) by A3, A5, Def4;

              then r <= ((f to_power k) . x) by A6, A8, POWER: 24;

              hence x in ( great_eq_dom ((f to_power k),r1)) by A3, A5, A9, MESFUNC6: 6;

            end;

            then E c= ( great_eq_dom ((f to_power k),r)) by TARSKI:def 3;

            then (E /\ ( great_eq_dom ((f to_power k),r))) = E by XBOOLE_1: 28;

            then (E /\ ( less_dom ((f to_power k),r1))) = (E \ E) by A7, Th28;

            hence (E /\ ( less_dom ((f to_power k),r))) in S;

          end;

            suppose

             A10: 1 < r;

            now

              let x be object;

              assume

               A11: x in E;

              then ((f to_power k) . x) = ((f . x) to_power k) by A3, A5, Def4;

              then ((f to_power k) . x) < r by A6, A10, POWER: 24;

              hence x in ( less_dom ((f to_power k),r)) by A3, A5, A11, MESFUNC6: 3;

            end;

            then E c= ( less_dom ((f to_power k),r)) by TARSKI:def 3;

            then (E /\ ( less_dom ((f to_power k),r))) = E by XBOOLE_1: 28;

            hence (E /\ ( less_dom ((f to_power k),r))) in S;

          end;

        end;

        hence thesis by MESFUNC6: 12;

      end;

        suppose

         A12: k > 0 ;

        for r be Real holds (E /\ ( great_eq_dom ((f to_power k),r))) in S

        proof

          let r be Real;

          reconsider r1 = r as Real;

          per cases ;

            suppose

             A13: r1 <= 0 ;

            now

              let x be object;

              assume x in E;

              then x in ( dom f) by A3;

              then

               A14: x in ( dom (f to_power k)) by Def4;

               0 <= ((f to_power k) . x) by A1, A12, MESFUNC6: 51;

              hence x in ( great_eq_dom ((f to_power k),r1)) by A13, A14, MESFUNC6: 6;

            end;

            then E c= ( great_eq_dom ((f to_power k),r)) by TARSKI:def 3;

            then (E /\ ( great_eq_dom ((f to_power k),r))) = E by XBOOLE_1: 28;

            hence thesis;

          end;

            suppose

             A15: 0 < r1;

             A16:

            now

              set R = (r to_power (jj / k));

              let x be object;

              reconsider xx = x as set by TARSKI: 1;

              

               A17: 0 < (r to_power (jj / k)) by A15, POWER: 34;

              assume

               A18: x in ( great_eq_dom (f,(r1 to_power (1 / k))));

              then

               A19: x in ( dom (f to_power k)) by A5, MESFUNC6: 6;

              (R to_power k) = (r to_power ((1 / k) * k)) by A15, POWER: 33;

              then

               A20: (R to_power k) = (r to_power 1) by A12, XCMPLX_1: 87;

              ex y be Real st y = (f . x) & (r1 to_power (1 / k)) <= y by A18, MESFUNC6: 6;

              then (r1 to_power jj) <= ((f . xx) to_power k1) by A12, A17, A20, HOLDER_1: 3;

              then r <= ((f . xx) to_power k) by POWER: 25;

              then r <= ((f to_power k) . xx) by A19, Def4;

              hence x in ( great_eq_dom ((f to_power k),r1)) by A19, MESFUNC6: 6;

            end;

            now

              let x be object;

              reconsider xx = x as set by TARSKI: 1;

              assume

               A21: x in ( great_eq_dom ((f to_power k),r1));

              then

               A22: x in ( dom (f to_power k)) by MESFUNC6: 6;

               0 <= (f . xx) by A1, MESFUNC6: 51;

              then (((f . xx) to_power k1) to_power (1 / k1)) = ((f . xx) to_power ((k1 * 1) / k1)) by A12, HOLDER_1: 2;

              then (((f . xx) to_power k1) to_power (1 / k1)) = ((f . xx) to_power 1) by A12, XCMPLX_1: 87;

              then

               A23: (((f . xx) to_power k) to_power (1 / k)) = (f . x) by POWER: 25;

              ex y2 be Real st y2 = ((f to_power k) . x) & r1 <= y2 by A21, MESFUNC6: 6;

              then r <= ((f . xx) to_power k) by A22, Def4;

              then (r to_power (1 / k1)) <= (((f . xx) to_power k1) to_power (1 / k1)) by A12, A15, HOLDER_1: 3;

              hence x in ( great_eq_dom (f,(r1 to_power (1 / k)))) by A5, A22, A23, MESFUNC6: 6;

            end;

            then (E /\ ( great_eq_dom ((f to_power k),r1))) = (E /\ ( great_eq_dom (f,(r1 to_power (1 / k))))) by A16, TARSKI: 2;

            hence thesis by A3, A4, MESFUNC6: 13;

          end;

        end;

        hence thesis by A3, A5, MESFUNC6: 13;

      end;

    end;

    theorem :: MESFUN6C:30

    

     Th30: f is A -measurable & A c= ( dom f) implies |.f.| is A -measurable

    proof

      assume that

       A1: f is A -measurable and

       A2: A c= ( dom f);

      

       A3: ( dom ( Im f)) = ( dom f) by COMSEQ_3:def 4;

       A4:

      now

        let x be object;

        assume x in ( dom |.( Im f).|);

        then ( |.( Im f).| . x) = |.(( Im f) . x) qua Complex.| by VALUED_1:def 11;

        hence 0 <= ( |.( Im f).| . x) by COMPLEX1: 46;

      end;

      then

       A5: ( |.( Im f).| to_power 2) is nonnegative by Th26, MESFUNC6: 52;

      

       A6: ( dom |.( Im f).|) = ( dom ( Im f)) by VALUED_1:def 11;

      then

       A7: ( dom ( |.( Im f).| to_power 2)) = ( dom f) by A3, Def4;

      ( Im f) is A -measurable by A1;

      then |.( Im f).| is A -measurable by A2, A3, MESFUNC6: 48;

      then

       A8: ( |.( Im f).| to_power 2) is A -measurable by A2, A6, A3, A4, Th29, MESFUNC6: 52;

      

       A9: ( dom ( Re f)) = ( dom f) by COMSEQ_3:def 3;

       A10:

      now

        let x be object;

        

         A11: 0 <= |.(( Re f) . x) qua Complex.| by COMPLEX1: 46;

        assume x in ( dom |.( Re f).|);

        hence 0 <= ( |.( Re f).| . x) by A11, VALUED_1:def 11;

      end;

      then

       A12: ( |.( Re f).| to_power 2) is nonnegative by Th26, MESFUNC6: 52;

      set F = (( |.( Re f).| to_power 2) + ( |.( Im f).| to_power 2));

      

       A13: ( dom |.f.|) = ( dom f) by VALUED_1:def 11;

      

       A14: ( dom |.( Re f).|) = ( dom ( Re f)) by VALUED_1:def 11;

      then

       A15: ( dom ( |.( Re f).| to_power 2)) = ( dom f) by A9, Def4;

      

       A16: ( dom F) = (( dom ( |.( Re f).| to_power 2)) /\ ( dom ( |.( Im f).| to_power 2))) by VALUED_1:def 1;

      then

       A17: ( dom |.f.|) = ( dom (F to_power (1 / 2))) by A13, A15, A7, Def4;

      now

        let x be object;

        assume

         A18: x in ( dom |.f.|);

        then (( |.( Re f).| to_power 2) . x) = (( |.( Re f).| . x) to_power 2) by A13, A15, Def4;

        then (( |.( Re f).| to_power 2) . x) = ( |.(( Re f) . x) qua Complex.| to_power 2) by A14, A13, A9, A18, VALUED_1:def 11;

        then (( |.( Re f).| to_power 2) . x) = ( |.( Re (f . x)) qua Complex.| to_power 2) by A13, A9, A18, COMSEQ_3:def 3;

        then (( |.( Re f).| to_power 2) . x) = ( |.( Re (f . x)) qua Complex.| ^2 ) by POWER: 46;

        then

         A19: (( |.( Re f).| to_power 2) . x) = (( Re (f . x)) ^2 ) by COMPLEX1: 75;

        (( |.( Im f).| to_power 2) . x) = (( |.( Im f).| . x) to_power 2) by A13, A7, A18, Def4;

        then (( |.( Im f).| to_power 2) . x) = ( |.(( Im f) . x) qua Complex.| to_power 2) by A6, A13, A3, A18, VALUED_1:def 11;

        then (( |.( Im f).| to_power 2) . x) = ( |.( Im (f . x)) qua Complex.| to_power 2) by A13, A3, A18, COMSEQ_3:def 4;

        then (( |.( Im f).| to_power 2) . x) = ( |.( Im (f . x)) qua Complex.| ^2 ) by POWER: 46;

        then

         A20: (( |.( Im f).| to_power 2) . x) = (( Im (f . x)) ^2 ) by COMPLEX1: 75;

        ((F . x) to_power (1 / 2)) = ( sqrt (F . x)) by A12, A5, Th27, MESFUNC6: 56

        .= ( sqrt ((( Re (f . x)) ^2 ) + (( Im (f . x)) ^2 ))) by A13, A16, A15, A7, A18, A19, A20, VALUED_1:def 1;

        then ((F to_power (1 / 2)) . x) = |.(f . x).| by A17, A18, Def4;

        hence ( |.f.| . x) = ((F to_power (1 / 2)) . x) by A18, VALUED_1:def 11;

      end;

      then

       A21: |.f.| = (F to_power (1 / 2)) by A17, FUNCT_1: 2;

      ( Re f) is A -measurable by A1;

      then |.( Re f).| is A -measurable by A2, A9, MESFUNC6: 48;

      then ( |.( Re f).| to_power 2) is A -measurable by A2, A14, A9, A10, Th29, MESFUNC6: 52;

      then F is A -measurable by A8, MESFUNC6: 26;

      hence thesis by A2, A12, A5, A16, A15, A7, A21, Th29, MESFUNC6: 56;

    end;

    theorem :: MESFUN6C:31

    

     Th31: (ex A be Element of S st A = ( dom f) & f is A -measurable) implies (f is_integrable_on M iff |.f.| is_integrable_on M)

    proof

      

       A1: ( dom ( |.( Re f).| + |.( Im f).|)) = (( dom |.( Re f).|) /\ ( dom |.( Im f).|)) by VALUED_1:def 1;

      

       A2: ( dom |.( Re f).|) = ( dom ( Re f)) by VALUED_1:def 11;

      

       A3: ( dom |.( Im f).|) = ( dom ( Im f)) by VALUED_1:def 11;

      

       A4: ( dom |.f.|) = ( dom f) by VALUED_1:def 11;

      assume ex A be Element of S st A = ( dom f) & f is A -measurable;

      then

      consider A be Element of S such that

       A5: A = ( dom f) and

       A6: f is A -measurable;

      

       A7: ( dom ( Re f)) = A by A5, COMSEQ_3:def 3;

      

       A8: ( Im f) is A -measurable by A6;

      

       A9: ( Re f) is A -measurable by A6;

      

       A10: ( dom ( Im f)) = A by A5, COMSEQ_3:def 4;

      

       A11: |.f.| is A -measurable by A5, A6, Th30;

      hereby

         A12:

        now

          let x be Element of X;

          assume

           A13: x in ( dom |.f.|);

          then

           A14: ( |.f.| . x) = |.(f . x).| by VALUED_1:def 11;

          

           A15: |.(( Im f) . x) qua Complex.| = ( |.( Im f).| . x) by A5, A10, A3, A4, A13, VALUED_1:def 11;

          

           A16: |.(( Re f) . x) qua Complex.| = ( |.( Re f).| . x) by A5, A7, A2, A4, A13, VALUED_1:def 11;

          

           A17: (( Im f) . x) = ( Im (f . x)) by A5, A10, A4, A13, COMSEQ_3:def 4;

          

           A18: (( Re f) . x) = ( Re (f . x)) by A5, A7, A4, A13, COMSEQ_3:def 3;

          (( |.( Re f).| + |.( Im f).|) . x) = (( |.( Re f).| . x) + ( |.( Im f).| . x)) by A5, A7, A10, A1, A2, A3, A4, A13, VALUED_1:def 1;

          hence |.( |.f.| . x) qua Complex.| <= (( |.( Re f).| + |.( Im f).|) . x) by A18, A17, A14, A16, A15, COMPLEX1: 78;

        end;

        assume

         A19: f is_integrable_on M;

        then ( Im f) is_integrable_on M;

        then

         A20: |.( Im f).| is_integrable_on M by A10, A8, MESFUNC6: 94;

        ( Re f) is_integrable_on M by A19;

        then |.( Re f).| is_integrable_on M by A7, A9, MESFUNC6: 94;

        then ( |.( Re f).| + |.( Im f).|) is_integrable_on M by A20, MESFUNC6: 100;

        hence |.f.| is_integrable_on M by A5, A7, A10, A1, A2, A3, A4, A11, A12, MESFUNC6: 96;

      end;

      hereby

        assume

         A21: |.f.| is_integrable_on M;

        now

          let x be Element of X;

          

           A22: |.( Im (f . x)) qua Complex.| <= |.(f . x).| by COMPLEX1: 79;

          assume

           A23: x in ( dom ( Im f));

          then ( |.f.| . x) = |.(f . x).| by A5, A10, A4, VALUED_1:def 11;

          hence |.(( Im f) . x) qua Complex.| <= ( |.f.| . x) by A23, A22, COMSEQ_3:def 4;

        end;

        then

         A24: ( Im f) is_integrable_on M by A5, A10, A8, A4, A21, MESFUNC6: 96;

        now

          let x be Element of X;

          

           A25: |.( Re (f . x)) qua Complex.| <= |.(f . x).| by COMPLEX1: 79;

          assume

           A26: x in ( dom ( Re f));

          then ( |.f.| . x) = |.(f . x).| by A5, A7, A4, VALUED_1:def 11;

          hence |.(( Re f) . x) qua Complex.| <= ( |.f.| . x) by A26, A25, COMSEQ_3:def 3;

        end;

        then ( Re f) is_integrable_on M by A5, A7, A9, A4, A21, MESFUNC6: 96;

        hence f is_integrable_on M by A24;

      end;

    end;

    theorem :: MESFUN6C:32

    f is_integrable_on M & g is_integrable_on M implies ( dom (f + g)) in S

    proof

      assume that

       A1: f is_integrable_on M and

       A2: g is_integrable_on M;

      

       A3: ( Re g) is_integrable_on M by A2;

      

       A4: ( Im g) is_integrable_on M by A2;

      ( Im f) is_integrable_on M by A1;

      then ( dom (( Im f) + ( Im g))) in S by A4, MESFUNC6: 99;

      then

       A5: ( dom ( Im (f + g))) in S by Th5;

      ( Re f) is_integrable_on M by A1;

      then ( dom (( Re f) + ( Re g))) in S by A3, MESFUNC6: 99;

      then

       A6: ( dom ( Re (f + g))) in S by Th5;

      ( dom ( <i> (#) ( Im (f + g)))) = ( dom ( Im (f + g))) by VALUED_1:def 5;

      then ( dom (( Re (f + g)) + ( <i> (#) ( Im (f + g))))) = (( dom ( Re (f + g))) /\ ( dom ( Im (f + g)))) by VALUED_1:def 1;

      then ( dom (( Re (f + g)) + ( <i> (#) ( Im (f + g))))) in S by A6, A5, FINSUB_1:def 2;

      hence thesis by Th8;

    end;

    theorem :: MESFUN6C:33

    

     Th33: f is_integrable_on M & g is_integrable_on M implies (f + g) is_integrable_on M

    proof

      assume that

       A1: f is_integrable_on M and

       A2: g is_integrable_on M;

      

       A3: ( Im g) is_integrable_on M by A2;

      ( Im f) is_integrable_on M by A1;

      then (( Im f) + ( Im g)) is_integrable_on M by A3, MESFUNC6: 100;

      then

       A4: ( Im (f + g)) is_integrable_on M by Th5;

      

       A5: ( Re g) is_integrable_on M by A2;

      ( Re f) is_integrable_on M by A1;

      then (( Re f) + ( Re g)) is_integrable_on M by A5, MESFUNC6: 100;

      then ( Re (f + g)) is_integrable_on M by Th5;

      hence thesis by A4;

    end;

    theorem :: MESFUN6C:34

    

     Th34: for X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f,g be PartFunc of X, REAL st f is_integrable_on M & g is_integrable_on M holds (f - g) is_integrable_on M

    proof

      let X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f,g be PartFunc of X, REAL ;

      assume that

       A1: f is_integrable_on M and

       A2: g is_integrable_on M;

      ( R_EAL g) is_integrable_on M by A2;

      then (( - jj) (#) ( R_EAL g)) is_integrable_on M by MESFUNC5: 110;

      then ( - ( R_EAL g)) is_integrable_on M by MESFUNC2: 9;

      then

       A3: ( R_EAL ( - g)) is_integrable_on M by MESFUNC6: 28;

      ( R_EAL f) is_integrable_on M by A1;

      then (( R_EAL f) + ( R_EAL ( - g))) is_integrable_on M by A3, MESFUNC5: 108;

      then ( R_EAL (f - g)) is_integrable_on M by MESFUNC6: 23;

      hence thesis;

    end;

    theorem :: MESFUN6C:35

    f is_integrable_on M & g is_integrable_on M implies (f - g) is_integrable_on M

    proof

      assume that

       A1: f is_integrable_on M and

       A2: g is_integrable_on M;

      

       A3: ( Im g) is_integrable_on M by A2;

      ( Im f) is_integrable_on M by A1;

      then (( Im f) - ( Im g)) is_integrable_on M by A3, Th34;

      then

       A4: ( Im (f - g)) is_integrable_on M by Th6;

      

       A5: ( Re g) is_integrable_on M by A2;

      ( Re f) is_integrable_on M by A1;

      then (( Re f) - ( Re g)) is_integrable_on M by A5, Th34;

      then ( Re (f - g)) is_integrable_on M by Th6;

      hence thesis by A4;

    end;

    theorem :: MESFUN6C:36

    

     Th36: f is_integrable_on M & g is_integrable_on M implies ex E be Element of S st E = (( dom f) /\ ( dom g)) & ( Integral (M,(f + g))) = (( Integral (M,(f | E))) + ( Integral (M,(g | E))))

    proof

      assume that

       A1: f is_integrable_on M and

       A2: g is_integrable_on M;

      

       A3: ( Re g) is_integrable_on M by A2;

      ( Re f) is_integrable_on M by A1;

      then

      consider E be Element of S such that

       A4: E = (( dom ( Re f)) /\ ( dom ( Re g))) and

       A5: ( Integral (M,(( Re f) + ( Re g)))) = (( Integral (M,(( Re f) | E))) + ( Integral (M,(( Re g) | E)))) by A3, MESFUNC6: 101;

      

       A6: (f | E) is_integrable_on M by A1, Th23;

      then

       A7: ( Re (f | E)) is_integrable_on M;

      then

       A8: ( Integral (M,( Re (f | E)))) < +infty by MESFUNC6: 90;

      

       A9: ( Im (f | E)) is_integrable_on M by A6;

      then

       A10: -infty < ( Integral (M,( Im (f | E)))) by MESFUNC6: 90;

      

       A11: ( Integral (M,( Im (f | E)))) < +infty by A9, MESFUNC6: 90;

       -infty < ( Integral (M,( Re (f | E)))) by A7, MESFUNC6: 90;

      then

      reconsider R1 = ( Integral (M,( Re (f | E)))), I1 = ( Integral (M,( Im (f | E)))) as Element of REAL by A8, A10, A11, XXREAL_0: 14;

      

       A12: ( dom f) = ( dom ( Re f)) by COMSEQ_3:def 3;

      

       A13: ( Im g) is_integrable_on M by A2;

      ( Im f) is_integrable_on M by A1;

      then

       A14: ex Ei be Element of S st Ei = (( dom ( Im f)) /\ ( dom ( Im g))) & ( Integral (M,(( Im f) + ( Im g)))) = (( Integral (M,(( Im f) | Ei))) + ( Integral (M,(( Im g) | Ei)))) by A13, MESFUNC6: 101;

      

       A15: ( Integral (M,(( Im f) + ( Im g)))) = ( Integral (M,( Im (f + g)))) by Th5;

      

       A16: (f + g) is_integrable_on M by A1, A2, Th33;

      then

       A17: ( Re (f + g)) is_integrable_on M;

      then

       A18: ( Integral (M,( Re (f + g)))) < +infty by MESFUNC6: 90;

      

       A19: ( Im (f + g)) is_integrable_on M by A16;

      then

       A20: -infty < ( Integral (M,( Im (f + g)))) by MESFUNC6: 90;

      

       A21: ( Integral (M,( Im (f + g)))) < +infty by A19, MESFUNC6: 90;

       -infty < ( Integral (M,( Re (f + g)))) by A17, MESFUNC6: 90;

      then

      reconsider R = ( Integral (M,( Re (f + g)))), I = ( Integral (M,( Im (f + g)))) as Element of REAL by A18, A20, A21, XXREAL_0: 14;

      

       A22: ( Integral (M,(f + g))) = (R + (I * <i> )) by A16, Def3;

      

       A23: ( dom g) = ( dom ( Im g)) by COMSEQ_3:def 4;

      

       A24: (g | E) is_integrable_on M by A2, Th23;

      then

       A25: ( Re (g | E)) is_integrable_on M;

      then

       A26: ( Integral (M,( Re (g | E)))) < +infty by MESFUNC6: 90;

      

       A27: ( Im (g | E)) is_integrable_on M by A24;

      then

       A28: -infty < ( Integral (M,( Im (g | E)))) by MESFUNC6: 90;

      

       A29: ( Integral (M,( Im (g | E)))) < +infty by A27, MESFUNC6: 90;

       -infty < ( Integral (M,( Re (g | E)))) by A25, MESFUNC6: 90;

      then

      reconsider R2 = ( Integral (M,( Re (g | E)))), I2 = ( Integral (M,( Im (g | E)))) as Element of REAL by A26, A28, A29, XXREAL_0: 14;

      

       A30: ( dom g) = ( dom ( Re g)) by COMSEQ_3:def 3;

      ( Integral (M,(( Re f) + ( Re g)))) = ( Integral (M,( Re (f + g)))) by Th5;

      

      then ( Integral (M,( Re (f + g)))) = (( Integral (M,( Re (f | E)))) + ( Integral (M,(( Re g) | E)))) by A5, Th7

      .= (( Integral (M,( Re (f | E)))) + ( Integral (M,( Re (g | E))))) by Th7;

      then

       A31: R = (R1 + R2) by SUPINF_2: 1;

      ( dom f) = ( dom ( Im f)) by COMSEQ_3:def 4;

      then ( Integral (M,( Im (f + g)))) = (( Integral (M,( Im (f | E)))) + ( Integral (M,(( Im g) | E)))) by A4, A12, A30, A23, A14, A15, Th7;

      then I = (I1 + I2 qua ExtReal) by Th7;

      then I = (I1 + I2);

      then ( Integral (M,(f + g))) = ((R1 + (I1 * <i> )) + (R2 + (I2 * <i> ))) by A31, A22;

      then ( Integral (M,(f + g))) = (( Integral (M,(f | E))) + (R2 + (I2 * <i> ))) by A6, Def3;

      then ( Integral (M,(f + g))) = (( Integral (M,(f | E))) + ( Integral (M,(g | E)))) by A24, Def3;

      hence thesis by A4, A12, A30;

    end;

    theorem :: MESFUN6C:37

    for X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f,g be PartFunc of X, REAL st f is_integrable_on M & g is_integrable_on M holds ex E be Element of S st E = (( dom f) /\ ( dom g)) & ( Integral (M,(f - g))) = (( Integral (M,(f | E))) + ( Integral (M,(( - g) | E))))

    proof

      let X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f,g be PartFunc of X, REAL ;

      assume that

       A1: f is_integrable_on M and

       A2: g is_integrable_on M;

      ( R_EAL g) is_integrable_on M by A2;

      then (( - jj) (#) ( R_EAL g)) is_integrable_on M by MESFUNC5: 110;

      then ( - ( R_EAL g)) is_integrable_on M by MESFUNC2: 9;

      then

       A3: ( R_EAL ( - g)) is_integrable_on M by MESFUNC6: 28;

      ( R_EAL f) is_integrable_on M by A1;

      then

      consider E be Element of S such that

       A4: E = (( dom ( R_EAL f)) /\ ( dom ( R_EAL ( - g)))) and

       A5: ( Integral (M,(( R_EAL f) + ( R_EAL ( - g))))) = (( Integral (M,(( R_EAL f) | E))) + ( Integral (M,(( R_EAL ( - g)) | E)))) by A3, MESFUNC5: 109;

      take E;

      ( dom ( R_EAL ( - g))) = ( dom ( - ( R_EAL g))) by MESFUNC6: 28;

      hence thesis by A4, A5, MESFUNC1:def 7, MESFUNC6: 23;

    end;

    theorem :: MESFUN6C:38

    

     Th38: f is_integrable_on M implies (r (#) f) is_integrable_on M & ( Integral (M,(r (#) f))) = (r * ( Integral (M,f)))

    proof

      

       A1: ( Integral (M,(r (#) ( Re f)))) = ( Integral (M,( Re (r (#) f)))) by Th2;

      

       A2: ( Integral (M,(r (#) ( Im f)))) = ( Integral (M,( Im (r (#) f)))) by Th2;

      assume

       A3: f is_integrable_on M;

      then

       A4: ( Re f) is_integrable_on M;

      then

       A5: ( Integral (M,( Re f))) < +infty by MESFUNC6: 90;

      (r (#) ( Re f)) is_integrable_on M by A4, MESFUNC6: 102;

      then

       A6: ( Re (r (#) f)) is_integrable_on M by Th2;

      then

       A7: ( Integral (M,( Re (r (#) f)))) < +infty by MESFUNC6: 90;

      

       A8: ( Im f) is_integrable_on M by A3;

      then

       A9: -infty < ( Integral (M,( Im f))) by MESFUNC6: 90;

      

       A10: ( Integral (M,( Im f))) < +infty by A8, MESFUNC6: 90;

       -infty < ( Integral (M,( Re f))) by A4, MESFUNC6: 90;

      then

      reconsider R1 = ( Integral (M,( Re f))), I1 = ( Integral (M,( Im f))) as Element of REAL by A5, A9, A10, XXREAL_0: 14;

      

       A11: (r qua ExtReal * R1) = (r * R1);

      

       A12: (r qua ExtReal * I1) = (r * I1);

      (r (#) ( Im f)) is_integrable_on M by A8, MESFUNC6: 102;

      then

       A13: ( Im (r (#) f)) is_integrable_on M by Th2;

      then

       A14: -infty < ( Integral (M,( Im (r (#) f)))) by MESFUNC6: 90;

      

       A15: ( Integral (M,( Im (r (#) f)))) < +infty by A13, MESFUNC6: 90;

       -infty < ( Integral (M,( Re (r (#) f)))) by A6, MESFUNC6: 90;

      then

      reconsider R2 = ( Integral (M,( Re (r (#) f)))), I2 = ( Integral (M,( Im (r (#) f)))) as Element of REAL by A7, A14, A15, XXREAL_0: 14;

      

       A16: ( Integral (M,(r (#) ( Im f)))) = (r * ( Integral (M,( Im f)))) by A8, MESFUNC6: 102;

      

       A17: (r (#) f) is_integrable_on M by A6, A13;

      ( Integral (M,(r (#) ( Re f)))) = (r qua ExtReal * ( Integral (M,( Re f)))) by A4, MESFUNC6: 102;

      then (R2 + (I2 * <i> )) = (r * (R1 + (I1 * <i> ))) by A16, A1, A2, A11, A12;

      then ( Integral (M,(r (#) f))) = (r * (R1 + (I1 * <i> ))) by A17, Def3;

      hence thesis by A3, A6, A13, Def3;

    end;

    theorem :: MESFUN6C:39

    

     Th39: f is_integrable_on M implies ( <i> (#) f) is_integrable_on M & ( Integral (M,( <i> (#) f))) = ( <i> * ( Integral (M,f)))

    proof

      

       A1: ( Re ( <i> (#) f)) = ( - ( Im f)) by Th4;

      assume

       A2: f is_integrable_on M;

      then

       A3: ( Im f) is_integrable_on M;

      

       A4: ( Im ( <i> (#) f)) = ( Re f) by Th4;

      then

       A5: ( Im ( <i> (#) f)) is_integrable_on M by A2;

      ( Re ( <i> (#) f)) is_integrable_on M by A3, A1, MESFUNC6: 102;

      hence ( <i> (#) f) is_integrable_on M by A5;

      then

      consider R1,I1 be Real such that

       A6: R1 = ( Integral (M,( Re ( <i> (#) f)))) and

       A7: I1 = ( Integral (M,( Im ( <i> (#) f)))) and

       A8: ( Integral (M,( <i> (#) f))) = (R1 + (I1 * <i> )) by Def3;

      consider R,I be Real such that

       A9: R = ( Integral (M,( Re f))) and

       A10: I = ( Integral (M,( Im f))) and

       A11: ( Integral (M,f)) = (R + (I * <i> )) by A2, Def3;

      R1 = (( - 1) * I qua ExtReal) by A3, A1, A10, A6, MESFUNC6: 102

      .= (( - 1) * I);

      hence thesis by A4, A9, A11, A7, A8;

    end;

    theorem :: MESFUN6C:40

    

     Th40: f is_integrable_on M implies (c (#) f) is_integrable_on M & ( Integral (M,(c (#) f))) = (c * ( Integral (M,f)))

    proof

      

       A1: c = (( Re c) + (( Im c) * <i> )) by COMPLEX1: 13;

      

       A2: ( dom ( <i> (#) f)) = ( dom f) by VALUED_1:def 5;

      assume

       A3: f is_integrable_on M;

      then

       A4: ( Integral (M,(( Re c) (#) f))) = (( Re c) * ( Integral (M,f))) by Th38;

      

       A5: ( <i> (#) f) is_integrable_on M by A3, Th39;

      then

       A6: (( Im c) (#) ( <i> (#) f)) is_integrable_on M by Th38;

      

       A7: (( Re c) (#) f) is_integrable_on M by A3, Th38;

      then

      consider E be Element of S such that

       A8: E = (( dom (( Re c) (#) f)) /\ ( dom (( Im c) (#) ( <i> (#) f)))) and

       A9: ( Integral (M,((( Re c) (#) f) + (( Im c) (#) ( <i> (#) f))))) = (( Integral (M,((( Re c) (#) f) | E))) + ( Integral (M,((( Im c) (#) ( <i> (#) f)) | E)))) by A6, Th36;

      

       A10: ( dom (c (#) f)) = ( dom f) by VALUED_1:def 5;

      

       A11: ( Integral (M,(( Im c) (#) ( <i> (#) f)))) = (( Im c) * ( Integral (M,( <i> (#) f)))) by A5, Th38;

      

       A12: ( dom (( Re c) (#) f)) = ( dom f) by VALUED_1:def 5;

      

       A13: ( dom (( Im c) (#) ( <i> (#) f))) = ( dom ( <i> (#) f)) by VALUED_1:def 5;

      

       A14: ( dom ((( Re c) (#) f) + (( Im c) (#) ( <i> (#) f)))) = (( dom (( Re c) (#) f)) /\ ( dom (( Im c) (#) ( <i> (#) f)))) by VALUED_1:def 1;

      now

        let x be Element of X;

        assume

         A15: x in ( dom (c (#) f));

        then

         A16: ((c (#) f) . x) = (c * (f . x)) by VALUED_1:def 5;

        

         A17: ((( Im c) (#) ( <i> (#) f)) . x) = (( Im c) * (( <i> (#) f) . x)) by A10, A2, A13, A15, VALUED_1:def 5;

        

         A18: ((( Re c) (#) f) . x) = (( Re c) * (f . x)) by A10, A12, A15, VALUED_1:def 5;

        

         A19: (( <i> (#) f) . x) = ( <i> * (f . x)) by A10, A2, A15, VALUED_1:def 5;

        (((( Re c) (#) f) + (( Im c) (#) ( <i> (#) f))) . x) = (((( Re c) (#) f) . x) + ((( Im c) (#) ( <i> (#) f)) . x)) by A10, A12, A2, A13, A14, A15, VALUED_1:def 1;

        hence ((c (#) f) . x) = (((( Re c) (#) f) + (( Im c) (#) ( <i> (#) f))) . x) by A1, A16, A18, A17, A19;

      end;

      then

       A20: (c (#) f) = ((( Re c) (#) f) + (( Im c) (#) ( <i> (#) f))) by A10, A12, A2, A13, A14, PARTFUN1: 5;

      hence (c (#) f) is_integrable_on M by A7, A6, Th33;

      

       A21: ( Integral (M,( <i> (#) f))) = ( <i> * ( Integral (M,f))) by A3, Th39;

      

      thus ( Integral (M,(c (#) f))) = ((( Re c) * ( Integral (M,f))) + ((( Im c) * <i> ) * ( Integral (M,f)))) by A12, A2, A13, A20, A4, A21, A11, A8, A9

      .= (c * ( Integral (M,f))) by A1;

    end;

    

     Lm2: (ex A be Element of S st A = ( dom f) & f is A -measurable) & f is_integrable_on M & ( Integral (M,f)) = 0 implies |.( Integral (M,f)).| <= ( Integral (M, |.f.|))

    proof

      assume that

       A1: ex A be Element of S st A = ( dom f) & f is A -measurable and

       A2: f is_integrable_on M and

       A3: ( Integral (M,f)) = 0 ;

      

       A4: |.f.| is_integrable_on M by A1, A2, Th31;

      consider R,I be Real such that

       A5: R = ( Integral (M,( Re f))) and I = ( Integral (M,( Im f))) and

       A6: ( Integral (M,f)) = (R + (I * <i> )) by A2, Def3;

      R = 0 by A3, A6, COMPLEX1: 4, COMPLEX1: 12;

      then

       A7: |.( Integral (M,( Re f))).| = 0 by A5, EXTREAL1: 16;

      ( Re f) is_integrable_on M by A2;

      then

       A8: |.( Integral (M,( Re f))).| <= ( Integral (M, |.( Re f).|)) by MESFUNC6: 95;

      

       A9: ( dom |.f.|) = ( dom f) by VALUED_1:def 11;

      consider A be Element of S such that

       A10: A = ( dom f) and

       A11: f is A -measurable by A1;

      

       A12: ( dom ( Re f)) = A by A10, COMSEQ_3:def 3;

       A13:

      now

        let x be Element of X;

        assume

         A14: x in ( dom ( Re f));

        then

         A15: (( Re f) . x) = ( Re (f . x)) by COMSEQ_3:def 3;

        ( |.f.| . x) = |.(f . x).| by A10, A12, A9, A14, VALUED_1:def 11;

        hence |.(( Re f) . x) qua Complex.| <= ( |.f.| . x) by A15, COMPLEX1: 79;

      end;

      ( Re f) is A -measurable by A11;

      hence thesis by A3, A4, A8, A10, A12, A9, A13, A7, COMPLEX1: 44, MESFUNC6: 96;

    end;

    theorem :: MESFUN6C:41

    

     Th41: for f be PartFunc of X, REAL , Y, r holds ((r (#) f) | Y) = (r (#) (f | Y))

    proof

      let f be PartFunc of X, REAL , Y, r;

      

       A1: ( dom ((r (#) f) | Y)) = (( dom (r (#) f)) /\ Y) by RELAT_1: 61

      .= (( dom f) /\ Y) by VALUED_1:def 5

      .= ( dom (f | Y)) by RELAT_1: 61;

      

       A2: ( dom ((r (#) f) | Y)) c= ( dom (r (#) f)) by RELAT_1: 60;

       A3:

      now

        let x be Element of X;

        assume

         A4: x in ( dom ((r (#) f) | Y));

        then x in ( dom (r (#) (f | Y))) by A1, VALUED_1:def 5;

        then ((r (#) (f | Y)) . x) = (r * ((f | Y) . x)) by VALUED_1:def 5;

        then ((r (#) (f | Y)) . x) = (r * (f . x)) by A1, A4, FUNCT_1: 47;

        then ((r (#) (f | Y)) . x) = ((r (#) f) . x) by A2, A4, VALUED_1:def 5;

        hence ((r (#) (f | Y)) . x) = (((r (#) f) | Y) . x) by A4, FUNCT_1: 47;

      end;

      ( dom ((r (#) f) | Y)) = ( dom (r (#) (f | Y))) by A1, VALUED_1:def 5;

      hence thesis by A3, PARTFUN1: 5;

    end;

    theorem :: MESFUN6C:42

    

     Th42: for f,g be PartFunc of X, REAL st (ex A be Element of S st A = (( dom f) /\ ( dom g)) & f is A -measurable & g is A -measurable) & f is_integrable_on M & g is_integrable_on M & (g - f) is nonnegative holds ex E be Element of S st E = (( dom f) /\ ( dom g)) & ( Integral (M,(f | E))) <= ( Integral (M,(g | E)))

    proof

      let f,g be PartFunc of X, REAL ;

      assume that

       A1: ex A be Element of S st A = (( dom f) /\ ( dom g)) & f is A -measurable & g is A -measurable and

       A2: f is_integrable_on M and

       A3: g is_integrable_on M and

       A4: (g - f) is nonnegative;

      set h = (( - 1) (#) f);

      h is_integrable_on M by A2, MESFUNC6: 102;

      then

      consider E be Element of S such that

       A5: E = (( dom h) /\ ( dom g)) and

       A6: ( Integral (M,(h + g))) = (( Integral (M,(h | E))) + ( Integral (M,(g | E)))) by A3, MESFUNC6: 101;

      

       A7: (f | E) is_integrable_on M by A2, MESFUNC6: 91;

      then

       A8: ( Integral (M,(f | E))) < +infty by MESFUNC6: 90;

       -infty < ( Integral (M,(f | E))) by A7, MESFUNC6: 90;

      then

      reconsider c1 = ( Integral (M,(f | E))) as Element of REAL by A8, XXREAL_0: 14;

      

       A9: (( - 1) * ( Integral (M,(f | E)))) = (( - 1) * c1) by EXTREAL1: 1;

      

       A10: (g | E) is_integrable_on M by A3, MESFUNC6: 91;

      then

       A11: ( Integral (M,(g | E))) < +infty by MESFUNC6: 90;

       -infty < ( Integral (M,(g | E))) by A10, MESFUNC6: 90;

      then

      reconsider c2 = ( Integral (M,(g | E))) as Element of REAL by A11, XXREAL_0: 14;

      take E;

      

       A12: (h | E) = (( - 1) (#) (f | E)) by Th41;

      consider A be Element of S such that

       A13: A = (( dom f) /\ ( dom g)) and

       A14: f is A -measurable and

       A15: g is A -measurable by A1;

      ( dom h) = ( dom f) by VALUED_1:def 5;

      then

       A16: ( dom (h + g)) = A by A13, VALUED_1:def 1;

      h is A -measurable by A13, A14, MESFUNC6: 21, XBOOLE_1: 17;

      then 0 <= (( Integral (M,(h | E))) + ( Integral (M,(g | E)))) by A4, A6, A15, A16, MESFUNC6: 26, MESFUNC6: 84;

      then 0 <= ((( - 1) * ( Integral (M,(f | E)))) + ( Integral (M,(g | E)))) by A7, A12, MESFUNC6: 102;

      then 0 <= (( - c1) + c2) by A9, SUPINF_2: 1;

      then ( 0 qua Real + c1) <= ((( - c1) + c2) + c1) by XREAL_1: 6;

      hence thesis by A5, VALUED_1:def 5;

    end;

    

     Lm3: (ex A be Element of S st A = ( dom f) & f is A -measurable) & f is_integrable_on M & ( Integral (M,f)) <> 0 implies |.( Integral (M,f)).| <= ( Integral (M, |.f.|))

    proof

      assume that

       A1: ex A be Element of S st A = ( dom f) & f is A -measurable and

       A2: f is_integrable_on M and

       A3: ( Integral (M,f)) <> 0 ;

      

       A4: |.f.| is_integrable_on M by A1, A2, Th31;

      set a = ( Integral (M,f));

       0 < |.a.| by A3, COMPLEX1: 47;

      then

       A5: ( |.a.| / |.a.|) = 1 by XCMPLX_1: 60;

      set h = (f (#) ( |.f.| " ));

      set b = (a / |.a.|);

      

       A6: ( dom |.f.|) = ( dom f) by VALUED_1:def 11;

      ( |.b.| * |.(b *' ).|) = |.(b * (b *' )).| by COMPLEX1: 65;

      then ( |.b.| * |.(b *' ).|) = |.(b * b).| by COMPLEX1: 69;

      then

       A7: ( |.b.| * |.(b *' ).|) = ( |.(a / |.a.|).| * |.(a / |.a.|).|) by COMPLEX1: 65;

      

       A8: h = (f /" |.f.|);

      then

       A9: ( dom h) = (( dom f) /\ ( dom |.f.|)) by VALUED_1: 16;

      then

       A10: ( dom ((b *' ) (#) h)) = ( dom f) by A6, VALUED_1:def 5;

      then

       A11: ( dom ( |.f.| (#) ((b *' ) (#) h))) = (( dom f) /\ ( dom f)) by A6, VALUED_1:def 4;

      then

       A12: ( dom ( Re ( |.f.| (#) ((b *' ) (#) h)))) = ( dom f) by COMSEQ_3:def 3;

      

       A13: ( dom ( |.f.| (#) h)) = (( dom |.f.|) /\ ( dom h)) by VALUED_1:def 4;

      then

       A14: ( dom ((b *' ) (#) ( |.f.| (#) h))) = ( dom f) by A6, A9, VALUED_1:def 5;

      now

        let x be object;

        assume

         A15: x in ( dom ((b *' ) (#) ( |.f.| (#) h)));

        then x in ( dom ( |.f.| (#) ((b *' ) (#) h))) by A6, A9, A13, A11, VALUED_1:def 5;

        then (( |.f.| (#) ((b *' ) (#) h)) . x) = (( |.f.| . x) * (((b *' ) (#) h) . x)) by VALUED_1:def 4;

        then (( |.f.| (#) ((b *' ) (#) h)) . x) = ( |.(f . x).| * (((b *' ) (#) h) . x)) by A6, A14, A15, VALUED_1:def 11;

        then

         A16: (( |.f.| (#) ((b *' ) (#) h)) . x) = (((b *' ) * (h . x)) * |.(f . x).|) by A14, A10, A15, VALUED_1:def 5;

        (((b *' ) (#) ( |.f.| (#) h)) . x) = ((b *' ) * (( |.f.| (#) h) . x)) by A15, VALUED_1:def 5;

        then (((b *' ) (#) ( |.f.| (#) h)) . x) = ((b *' ) * (( |.f.| . x) * (h . x))) by A6, A9, A13, A14, A15, VALUED_1:def 4;

        then (((b *' ) (#) ( |.f.| (#) h)) . x) = ((b *' ) * ( |.(f . x).| * (h . x))) by A6, A14, A15, VALUED_1:def 11;

        hence (((b *' ) (#) ( |.f.| (#) h)) . x) = (( |.f.| (#) ((b *' ) (#) h)) . x) by A16;

      end;

      then

       A17: ((b *' ) (#) ( |.f.| (#) h)) = ( |.f.| (#) ((b *' ) (#) h)) by A14, A11, FUNCT_1: 2;

      

       A18: |.(a / |.a qua Complex.|) qua Complex.| = ( |.a.| / |. |.a qua Complex.| qua Complex.|) by COMPLEX1: 67;

      now

        let x be set;

        

         A19: (h . x) = ((f . x) / ( |.f.| . x)) by A8, VALUED_1: 17;

        assume

         A20: x in (( dom ( Re ( |.f.| (#) ((b *' ) (#) h)))) /\ ( dom |.f.|));

        then ( |.f.| . x) = |.(f . x).| by A6, A12, VALUED_1:def 11;

        then

         A21: |.(h . x).| = ( |.(f . x).| / |. |.(f . x).| qua Complex.|) by A19, COMPLEX1: 67;

        per cases ;

          suppose

           A22: (f . x) <> 0 ;

          

           A23: ( Re (( |.f.| (#) ((b *' ) (#) h)) . x)) = (( Re ( |.f.| (#) ((b *' ) (#) h))) . x) by A6, A12, A20, COMSEQ_3:def 3;

          (( |.f.| (#) ((b *' ) (#) h)) . x) = (( |.f.| . x) * (((b *' ) (#) h) . x)) by A6, A11, A12, A20, VALUED_1:def 4;

          then (( |.f.| (#) ((b *' ) (#) h)) . x) = ( |.(f . x).| * (((b *' ) (#) h) . x)) by A6, A12, A20, VALUED_1:def 11;

          then

           A24: |.(( |.f.| (#) ((b *' ) (#) h)) . x) qua Complex.| = ( |. |.(f . x).| qua Complex.| * |.(((b *' ) (#) h) . x) qua Complex.|) by COMPLEX1: 65;

          x in ( dom ((b *' ) (#) h)) by A9, A12, A20, VALUED_1:def 5;

          then (((b *' ) (#) h) . x) = ((b *' ) * (h . x)) by VALUED_1:def 5;

          then

           A25: |.(((b *' ) (#) h) . x).| = ( |.(b *' ).| * |.(h . x).|) by COMPLEX1: 65;

           0 < |.(f . x).| by A22, COMPLEX1: 47;

          then ( |.(f . x).| / |.(f . x).|) = 1 by XCMPLX_1: 60;

          then ( Re (( |.f.| (#) ((b *' ) (#) h)) . x)) <= |.(f . x).| by A7, A18, A5, A21, A25, A24, COMPLEX1: 54;

          hence (( Re ( |.f.| (#) ((b *' ) (#) h))) . x) <= ( |.f.| . x) by A6, A12, A20, A23, VALUED_1:def 11;

        end;

          suppose

           A26: (f . x) = 0 ;

          (( |.f.| (#) ((b *' ) (#) h)) . x) = (( |.f.| . x) * (((b *' ) (#) h) . x)) by A6, A11, A12, A20, VALUED_1:def 4;

          then (( |.f.| (#) ((b *' ) (#) h)) . x) = ( |.(f . x).| * (((b *' ) (#) h) . x)) by A6, A12, A20, VALUED_1:def 11;

          then

           A27: |.(( |.f.| (#) ((b *' ) (#) h)) . x) qua Complex.| = ( |. |.(f . x) qua Complex.| qua Complex.| * |.(((b *' ) (#) h) . x) qua Complex.|) by COMPLEX1: 65;

          ((( Re (f . x)) ^2 ) + (( Im (f . x)) ^2 )) = 0 by A26, COMPLEX1: 5;

          then

           A28: ( Re (( |.f.| (#) ((b *' ) (#) h)) . x)) <= |.(f . x) qua Complex.| by A27, COMPLEX1: 54, SQUARE_1: 17;

          ( Re (( |.f.| (#) ((b *' ) (#) h)) . x)) = (( Re ( |.f.| (#) ((b *' ) (#) h))) . x) by A6, A12, A20, COMSEQ_3:def 3;

          hence (( Re ( |.f.| (#) ((b *' ) (#) h))) . x) <= ( |.f.| . x) by A6, A12, A20, A28, VALUED_1:def 11;

        end;

      end;

      then

       A29: ( |.f.| - ( Re ( |.f.| (#) ((b *' ) (#) h)))) is nonnegative by MESFUNC6: 58;

      set F = ( Re ( |.f.| (#) ((b *' ) (#) h)));

      reconsider b1 = b as Element of COMPLEX by XCMPLX_0:def 2;

      

       A30: ( Re (b1 * (b1 *' ))) = ((( Re b1) ^2 ) + (( Im b1) ^2 )) by COMPLEX1: 40;

      consider A be Element of S such that

       A31: A = ( dom f) and

       A32: f is A -measurable by A1;

      

       A33: |.f.| is A -measurable by A31, A32, Th30;

       A34:

      now

        let x be object;

        

         A35: (h . x) = ((f . x) / ( |.f.| . x)) by A8, VALUED_1: 17;

        assume

         A36: x in ( dom f);

        then

         A37: ( |.f.| . x) = |.(f . x).| by A6, VALUED_1:def 11;

        

         A38: (( |.f.| (#) h) . x) = (( |.f.| . x) * (h . x)) by A6, A9, A13, A36, VALUED_1:def 4;

        per cases ;

          suppose (f . x) <> 0 ;

          then 0 < |.(f . x).| by COMPLEX1: 47;

          hence (f . x) = (( |.f.| (#) h) . x) by A38, A37, A35, XCMPLX_1: 87;

        end;

          suppose

           A39: (f . x) = 0 ;

          then ((( Re (f . x)) ^2 ) + (( Im (f . x)) ^2 )) = 0 by COMPLEX1: 5;

          then (f . x) = ((h . x) * |.(f . x).|) by A39, SQUARE_1: 17;

          hence (f . x) = (( |.f.| (#) h) . x) by A6, A36, A38, VALUED_1:def 11;

        end;

      end;

      then

       A40: f = ( |.f.| (#) h) by A6, A9, A13, FUNCT_1: 2;

      then

       A41: ((b *' ) (#) ( |.f.| (#) h)) is_integrable_on M by A2, Th40;

      then

      consider R1,I1 be Real such that

       A42: R1 = ( Integral (M,( Re ( |.f.| (#) ((b *' ) (#) h))))) and I1 = ( Integral (M,( Im ( |.f.| (#) ((b *' ) (#) h))))) and

       A43: ( Integral (M,( |.f.| (#) ((b *' ) (#) h)))) = (R1 + (I1 * <i> )) by A17, Def3;

      

       A44: ( Im (b1 * (b1 *' ))) = 0 by COMPLEX1: 40;

      reconsider aa = |.a.| as Element of REAL by XREAL_0:def 1;

      (b * (b *' )) = (( Re (b * (b *' ))) + (( Im (b * (b *' ))) * <i> )) by COMPLEX1: 13;

      then (b * (b *' )) = |.(b * b) qua Complex.| by A30, A44, COMPLEX1: 68;

      then (((b *' ) * a) / |.a qua Complex.|) = 1 by A7, A18, A5, COMPLEX1: 65;

      then

       A45: ((b *' ) * a) = |.a.| by XCMPLX_1: 58;

      ( Re (R1 + (I1 * <i> ))) = R1 by COMPLEX1: 12;

      then ( Re |.aa qua Complex.|) = R1 by A2, A45, A40, A17, A43, Th40;

      then

       A46: |.aa qua Complex.| = ( Integral (M,( Re ( |.f.| (#) ((b *' ) (#) h))))) by A42, COMPLEX1:def 1;

      ( |.f.| (#) h) is A -measurable by A32, A6, A9, A13, A34, FUNCT_1: 2;

      then ((b *' ) (#) ( |.f.| (#) h)) is A -measurable by A31, A6, A9, A13, Th17;

      then

       A47: ( Re ( |.f.| (#) ((b *' ) (#) h))) is A -measurable by A17;

      ( Re ( |.f.| (#) ((b *' ) (#) h))) is_integrable_on M by A17, A41;

      then

      consider E be Element of S such that

       A48: E = (( dom F) /\ ( dom |.f.|)) and

       A49: ( Integral (M,(F | E))) <= ( Integral (M,( |.f.| | E))) by A4, A31, A6, A33, A47, A12, A29, Th42;

      thus thesis by A6, A46, A12, A48, A49;

    end;

    theorem :: MESFUN6C:43

    (ex A be Element of S st A = ( dom f) & f is A -measurable) & f is_integrable_on M implies |.( Integral (M,f)).| <= ( Integral (M, |.f.|))

    proof

      assume that

       A1: ex A be Element of S st A = ( dom f) & f is A -measurable and

       A2: f is_integrable_on M;

      per cases ;

        suppose ( Integral (M,f)) = 0 ;

        hence thesis by A1, A2, Lm2;

      end;

        suppose ( Integral (M,f)) <> 0 ;

        hence thesis by A1, A2, Lm3;

      end;

    end;

    definition

      let X be non empty set;

      let S be SigmaField of X;

      let M be sigma_Measure of S;

      let f be PartFunc of X, COMPLEX ;

      let B be Element of S;

      :: MESFUN6C:def5

      func Integral_on (M,B,f) -> Complex equals ( Integral (M,(f | B)));

      coherence ;

    end

    theorem :: MESFUN6C:44

    f is_integrable_on M & g is_integrable_on M & B c= ( dom (f + g)) implies (f + g) is_integrable_on M & ( Integral_on (M,B,(f + g))) = (( Integral_on (M,B,f)) + ( Integral_on (M,B,g)))

    proof

      assume that

       A1: f is_integrable_on M and

       A2: g is_integrable_on M and

       A3: B c= ( dom (f + g));

      

       A4: ( Re f) is_integrable_on M by A1;

      then (( Re f) | B) is_integrable_on M by MESFUNC6: 91;

      then

       A5: ( Re (f | B)) is_integrable_on M by Th7;

      then

       A6: ( Integral (M,( Re (f | B)))) < +infty by MESFUNC6: 90;

      

       A7: ( Im f) is_integrable_on M by A1;

      then (( Im f) | B) is_integrable_on M by MESFUNC6: 91;

      then

       A8: ( Im (f | B)) is_integrable_on M by Th7;

      then

       A9: -infty < ( Integral (M,( Im (f | B)))) by MESFUNC6: 90;

      

       A10: ( Integral (M,( Im (f | B)))) < +infty by A8, MESFUNC6: 90;

       -infty < ( Integral (M,( Re (f | B)))) by A5, MESFUNC6: 90;

      then

      reconsider R1 = ( Integral (M,( Re (f | B)))), I1 = ( Integral (M,( Im (f | B)))) as Element of REAL by A6, A9, A10, XXREAL_0: 14;

      (f | B) is_integrable_on M by A5, A8;

      then

       A11: ( Integral (M,(f | B))) = (R1 + (I1 * <i> )) by Def3;

      

       A12: ( Im g) is_integrable_on M by A2;

      then (( Im g) | B) is_integrable_on M by MESFUNC6: 91;

      then

       A13: ( Im (g | B)) is_integrable_on M by Th7;

      then

       A14: -infty < ( Integral (M,( Im (g | B)))) by MESFUNC6: 90;

      

       A15: ( Re g) is_integrable_on M by A2;

      then (( Re g) | B) is_integrable_on M by MESFUNC6: 91;

      then

       A16: ( Re (g | B)) is_integrable_on M by Th7;

      then

       A17: ( Integral (M,( Re (g | B)))) < +infty by MESFUNC6: 90;

      B c= ( dom ( Im (f + g))) by A3, COMSEQ_3:def 4;

      then

       A18: B c= ( dom (( Im f) + ( Im g))) by Th5;

      then ( Integral_on (M,B,(( Im f) + ( Im g)))) = (( Integral_on (M,B,( Im f))) + ( Integral_on (M,B,( Im g)))) by A7, A12, MESFUNC6: 103;

      then

       A19: ( Integral (M,(( Im (f + g)) | B))) = (( Integral (M,(( Im f) | B))) + ( Integral (M,(( Im g) | B)))) by Th5;

      

       A20: ( Integral (M,( Im (g | B)))) < +infty by A13, MESFUNC6: 90;

       -infty < ( Integral (M,( Re (g | B)))) by A16, MESFUNC6: 90;

      then

      reconsider R2 = ( Integral (M,( Re (g | B)))), I2 = ( Integral (M,( Im (g | B)))) as Element of REAL by A17, A14, A20, XXREAL_0: 14;

      (g | B) is_integrable_on M by A16, A13;

      then

       A21: ( Integral (M,(g | B))) = (R2 + (I2 * <i> )) by Def3;

      

       A22: ( Integral (M,(( Im g) | B))) = I2 by Th7;

      (( Im f) + ( Im g)) is_integrable_on M by A7, A12, A18, MESFUNC6: 103;

      then

       A23: ( Im (f + g)) is_integrable_on M by Th5;

      then (( Im (f + g)) | B) is_integrable_on M by MESFUNC6: 91;

      then

       A24: ( Im ((f + g) | B)) is_integrable_on M by Th7;

      then

       A25: -infty < ( Integral (M,( Im ((f + g) | B)))) by MESFUNC6: 90;

      B c= ( dom ( Re (f + g))) by A3, COMSEQ_3:def 3;

      then

       A26: B c= ( dom (( Re f) + ( Re g))) by Th5;

      then ( Integral_on (M,B,(( Re f) + ( Re g)))) = (( Integral_on (M,B,( Re f))) + ( Integral_on (M,B,( Re g)))) by A4, A15, MESFUNC6: 103;

      then

       A27: ( Integral (M,(( Re (f + g)) | B))) = (( Integral (M,(( Re f) | B))) + ( Integral (M,(( Re g) | B)))) by Th5;

      (( Re f) + ( Re g)) is_integrable_on M by A4, A15, A26, MESFUNC6: 103;

      then

       A28: ( Re (f + g)) is_integrable_on M by Th5;

      then (( Re (f + g)) | B) is_integrable_on M by MESFUNC6: 91;

      then

       A29: ( Re ((f + g) | B)) is_integrable_on M by Th7;

      then

       A30: ( Integral (M,( Re ((f + g) | B)))) < +infty by MESFUNC6: 90;

      

       A31: ( Integral (M,( Im ((f + g) | B)))) < +infty by A24, MESFUNC6: 90;

       -infty < ( Integral (M,( Re ((f + g) | B)))) by A29, MESFUNC6: 90;

      then

      reconsider R = ( Integral (M,( Re ((f + g) | B)))), I = ( Integral (M,( Im ((f + g) | B)))) as Element of REAL by A30, A25, A31, XXREAL_0: 14;

      

       A32: ( Integral (M,(( Re g) | B))) = R2 by Th7;

      ( Integral (M,(( Im f) | B))) = I1 by Th7;

      then I = (I1 + I2 qua ExtReal) by A19, A22, Th7;

      then

       A33: I = (I1 + I2);

      ( Integral (M,(( Re f) | B))) = R1 by Th7;

      then R = (R1 + R2 qua ExtReal) by A27, A32, Th7;

      then

       A34: R = (R1 + R2);

      ((f + g) | B) is_integrable_on M by A29, A24;

      

      then ( Integral_on (M,B,(f + g))) = (R + (I * <i> )) by Def3

      .= (( Integral_on (M,B,f)) + ( Integral_on (M,B,g))) by A34, A33, A11, A21;

      hence thesis by A28, A23;

    end;

    theorem :: MESFUN6C:45

    f is_integrable_on M implies ( Integral_on (M,B,(c (#) f))) = (c * ( Integral_on (M,B,f)))

    proof

      assume f is_integrable_on M;

      then

       A1: (f | B) is_integrable_on M by Th23;

      

       A2: ( dom ((c (#) f) | B)) = (( dom (c (#) f)) /\ B) by RELAT_1: 61;

      then ( dom ((c (#) f) | B)) = (( dom f) /\ B) by VALUED_1:def 5;

      then

       A3: ( dom ((c (#) f) | B)) = ( dom (f | B)) by RELAT_1: 61;

       A4:

      now

        let x be object;

        assume

         A5: x in ( dom ((c (#) f) | B));

        then

         A6: (((c (#) f) | B) . x) = ((c (#) f) . x) by FUNCT_1: 47;

        x in ( dom (c (#) f)) by A2, A5, XBOOLE_0:def 4;

        then (((c (#) f) | B) . x) = (c * (f . x)) by A6, VALUED_1:def 5;

        then

         A7: (((c (#) f) | B) . x) = (c * ((f | B) . x)) by A3, A5, FUNCT_1: 47;

        x in ( dom (c (#) (f | B))) by A3, A5, VALUED_1:def 5;

        hence (((c (#) f) | B) . x) = ((c (#) (f | B)) . x) by A7, VALUED_1:def 5;

      end;

      ( dom ((c (#) f) | B)) = ( dom (c (#) (f | B))) by A3, VALUED_1:def 5;

      then ((c (#) f) | B) = (c (#) (f | B)) by A4, FUNCT_1: 2;

      hence thesis by A1, Th40;

    end;

    begin

    reserve f for PartFunc of X, REAL ,

a for Real;

    theorem :: MESFUN6C:46

    for f be PartFunc of X, REAL , a be Real st A c= ( dom f) holds (A /\ ( great_eq_dom (f,a))) = (A \ (A /\ ( less_dom (f,a))))

    proof

      let f be PartFunc of X, REAL , a be Real;

      now

        let x be object;

        assume

         A1: x in (A /\ ( great_eq_dom (f,a)));

        then x in ( great_eq_dom (f,a)) by XBOOLE_0:def 4;

        then ex y be Real st y = (f . x) & a <= y by MESFUNC6: 6;

        then not (ex y1 be Real st y1 = (f . x) & y1 < a);

        then not x in ( less_dom (f,a)) by MESFUNC6: 3;

        then

         A2: not x in (A /\ ( less_dom (f,a))) by XBOOLE_0:def 4;

        x in A by A1, XBOOLE_0:def 4;

        hence x in (A \ (A /\ ( less_dom (f,a)))) by A2, XBOOLE_0:def 5;

      end;

      then

       A3: (A /\ ( great_eq_dom (f,a))) c= (A \ (A /\ ( less_dom (f,a)))) by TARSKI:def 3;

      assume

       A4: A c= ( dom f);

      now

        let x be object;

        assume

         A5: x in (A \ (A /\ ( less_dom (f,a))));

        then

         A6: x in A by XBOOLE_0:def 5;

         not x in (A /\ ( less_dom (f,a))) by A5, XBOOLE_0:def 5;

        then not x in ( less_dom (f,a)) by A6, XBOOLE_0:def 4;

        then not (f . x) < a by A4, A6, MESFUNC6: 3;

        then x in ( great_eq_dom (f,a)) by A4, A6, MESFUNC6: 6;

        hence x in (A /\ ( great_eq_dom (f,a))) by A6, XBOOLE_0:def 4;

      end;

      then (A \ (A /\ ( less_dom (f,a)))) c= (A /\ ( great_eq_dom (f,a))) by TARSKI:def 3;

      hence thesis by A3, XBOOLE_0:def 10;

    end;

    theorem :: MESFUN6C:47

    for f be PartFunc of X, REAL , a be Real st A c= ( dom f) holds (A /\ ( great_dom (f,a))) = (A \ (A /\ ( less_eq_dom (f,a))))

    proof

      let f be PartFunc of X, REAL , a be Real;

      now

        let x be object;

        assume

         A1: x in (A /\ ( great_dom (f,a)));

        then x in ( great_dom (f,a)) by XBOOLE_0:def 4;

        then ex y be Real st y = (f . x) & a < y by MESFUNC6: 5;

        then not (ex y1 be Real st y1 = (f . x) & y1 <= a);

        then not x in ( less_eq_dom (f,a)) by MESFUNC6: 4;

        then

         A2: not x in (A /\ ( less_eq_dom (f,a))) by XBOOLE_0:def 4;

        x in A by A1, XBOOLE_0:def 4;

        hence x in (A \ (A /\ ( less_eq_dom (f,a)))) by A2, XBOOLE_0:def 5;

      end;

      then

       A3: (A /\ ( great_dom (f,a))) c= (A \ (A /\ ( less_eq_dom (f,a)))) by TARSKI:def 3;

      assume

       A4: A c= ( dom f);

      now

        let x be object;

        assume

         A5: x in (A \ (A /\ ( less_eq_dom (f,a))));

        then

         A6: x in A by XBOOLE_0:def 5;

         not x in (A /\ ( less_eq_dom (f,a))) by A5, XBOOLE_0:def 5;

        then not x in ( less_eq_dom (f,a)) by A6, XBOOLE_0:def 4;

        then not (f . x) <= a by A4, A6, MESFUNC6: 4;

        then x in ( great_dom (f,a)) by A4, A6, MESFUNC6: 5;

        hence x in (A /\ ( great_dom (f,a))) by A6, XBOOLE_0:def 4;

      end;

      then (A \ (A /\ ( less_eq_dom (f,a)))) c= (A /\ ( great_dom (f,a))) by TARSKI:def 3;

      hence thesis by A3, XBOOLE_0:def 10;

    end;

    theorem :: MESFUN6C:48

    for f be PartFunc of X, REAL , a be Real st A c= ( dom f) holds (A /\ ( less_eq_dom (f,a))) = (A \ (A /\ ( great_dom (f,a))))

    proof

      let f be PartFunc of X, REAL , a be Real;

      now

        let x be object;

        assume

         A1: x in (A /\ ( less_eq_dom (f,a)));

        then x in ( less_eq_dom (f,a)) by XBOOLE_0:def 4;

        then ex y be Real st y = (f . x) & y <= a by MESFUNC6: 4;

        then not (ex y1 be Real st y1 = (f . x) & a < y1);

        then not x in ( great_dom (f,a)) by MESFUNC6: 5;

        then

         A2: not x in (A /\ ( great_dom (f,a))) by XBOOLE_0:def 4;

        x in A by A1, XBOOLE_0:def 4;

        hence x in (A \ (A /\ ( great_dom (f,a)))) by A2, XBOOLE_0:def 5;

      end;

      then

       A3: (A /\ ( less_eq_dom (f,a))) c= (A \ (A /\ ( great_dom (f,a)))) by TARSKI:def 3;

      assume

       A4: A c= ( dom f);

      now

        let x be object;

        assume

         A5: x in (A \ (A /\ ( great_dom (f,a))));

        then

         A6: x in A by XBOOLE_0:def 5;

         not x in (A /\ ( great_dom (f,a))) by A5, XBOOLE_0:def 5;

        then not x in ( great_dom (f,a)) by A6, XBOOLE_0:def 4;

        then not a < (f . x) by A4, A6, MESFUNC6: 5;

        then x in ( less_eq_dom (f,a)) by A4, A6, MESFUNC6: 4;

        hence x in (A /\ ( less_eq_dom (f,a))) by A6, XBOOLE_0:def 4;

      end;

      then (A \ (A /\ ( great_dom (f,a)))) c= (A /\ ( less_eq_dom (f,a))) by TARSKI:def 3;

      hence thesis by A3, XBOOLE_0:def 10;

    end;

    theorem :: MESFUN6C:49

    (A /\ ( eq_dom (f,a))) = ((A /\ ( great_eq_dom (f,a))) /\ ( less_eq_dom (f,a)))

    proof

      now

        let x be object;

        assume

         A1: x in ((A /\ ( great_eq_dom (f,a))) /\ ( less_eq_dom (f,a)));

        then

         A2: x in ( less_eq_dom (f,a)) by XBOOLE_0:def 4;

        then

         A3: x in ( dom f) by MESFUNC6: 4;

        

         A4: x in (A /\ ( great_eq_dom (f,a))) by A1, XBOOLE_0:def 4;

        then x in ( great_eq_dom (f,a)) by XBOOLE_0:def 4;

        then

         A5: ex y1 be Real st y1 = (f . x) & a <= y1 by MESFUNC6: 6;

        ex y2 be Real st y2 = (f . x) & y2 <= a by A2, MESFUNC6: 4;

        then a = (f . x) by A5, XXREAL_0: 1;

        then

         A6: x in ( eq_dom (f,a)) by A3, MESFUNC6: 7;

        x in A by A4, XBOOLE_0:def 4;

        hence x in (A /\ ( eq_dom (f,a))) by A6, XBOOLE_0:def 4;

      end;

      then

       A7: ((A /\ ( great_eq_dom (f,a))) /\ ( less_eq_dom (f,a))) c= (A /\ ( eq_dom (f,a))) by TARSKI:def 3;

      now

        let x be object;

        assume

         A8: x in (A /\ ( eq_dom (f,a)));

        then

         A9: x in A by XBOOLE_0:def 4;

        

         A10: x in ( eq_dom (f,a)) by A8, XBOOLE_0:def 4;

        then

         A11: ex y be Real st y = (f . x) & a = y by MESFUNC6: 7;

        

         A12: x in ( dom f) by A10, MESFUNC6: 7;

        then x in ( great_eq_dom (f,a)) by A11, MESFUNC6: 6;

        then

         A13: x in (A /\ ( great_eq_dom (f,a))) by A9, XBOOLE_0:def 4;

        x in ( less_eq_dom (f,a)) by A11, A12, MESFUNC6: 4;

        hence x in ((A /\ ( great_eq_dom (f,a))) /\ ( less_eq_dom (f,a))) by A13, XBOOLE_0:def 4;

      end;

      then (A /\ ( eq_dom (f,a))) c= ((A /\ ( great_eq_dom (f,a))) /\ ( less_eq_dom (f,a))) by TARSKI:def 3;

      hence thesis by A7, XBOOLE_0:def 10;

    end;