mesfunc6.miz



    begin

    reserve X for non empty set,

Y for set,

S for SigmaField of X,

F for sequence of S,

f,g for PartFunc of X, REAL ,

A,B for Element of S,

r,s for Real,

a for Real,

n for Nat;

    theorem :: MESFUNC6:1

    

     Th1: |.( R_EAL f).| = ( R_EAL ( abs f))

    proof

       A1:

      now

        let x be Element of X;

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

        then ( |.( R_EAL f).| . x) = |.(( R_EAL f) . x).| by MESFUNC1:def 10;

        then ( |.( R_EAL f).| . x) = |.(f . x) qua Complex.| by EXTREAL1: 12;

        then ( |.( R_EAL f).| . x) = ( |.f.| . x) by VALUED_1: 18;

        hence ( |.( R_EAL f).| . x) = (( R_EAL ( abs f)) . x);

      end;

      ( dom |.( R_EAL f).|) = ( dom ( R_EAL f)) by MESFUNC1:def 10

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

      hence thesis by A1, PARTFUN1: 5;

    end;

    theorem :: MESFUNC6:2

    

     Th2: for X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f be PartFunc of X, ExtREAL , r be Real st ( dom f) in S & (for x be object st x in ( dom f) holds (f . x) = r) holds f is_simple_func_in S

    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 ;

      let r be Real;

      assume that

       A1: ( dom f) in S and

       A2: for x be object st x in ( dom f) holds (f . x) = r;

      reconsider Df = ( dom f) as Element of S by A1;

      

       A3: ex F be Finite_Sep_Sequence of S st (( dom f) = ( union ( rng F)) & for n be Nat, x,y be Element of X st n in ( dom F) & x in (F . n) & y in (F . n) holds (f . x) = (f . y))

      proof

        set F = <*Df*>;

        

         A4: ( dom F) = ( Seg 1) by FINSEQ_1: 38;

         A5:

        now

          let i,j be Nat;

          assume that

           A6: i in ( dom F) and

           A7: j in ( dom F) & i <> j;

          i = 1 by A4, A6, FINSEQ_1: 2, TARSKI:def 1;

          hence (F . i) misses (F . j) by A4, A7, FINSEQ_1: 2, TARSKI:def 1;

        end;

        

         A8: for n be Nat st n in ( dom F) holds (F . n) = Df

        proof

          let n be Nat;

          assume n in ( dom F);

          then n = 1 by A4, FINSEQ_1: 2, TARSKI:def 1;

          hence thesis by FINSEQ_1: 40;

        end;

        reconsider F as Finite_Sep_Sequence of S by A5, MESFUNC3: 4;

        take F;

        F = <*(F . 1)*> by FINSEQ_1: 40;

        then

         A9: ( rng F) = {(F . 1)} by FINSEQ_1: 38;

        1 in ( Seg 1);

        then (F . 1) = Df by A4, A8;

        hence ( dom f) = ( union ( rng F)) by A9, ZFMISC_1: 25;

        hereby

          let n be Nat, x,y be Element of X;

          assume that

           A10: n in ( dom F) and

           A11: x in (F . n) and

           A12: y in (F . n);

          

           A13: (F . n) = Df by A8, A10;

          then (f . x) = r by A2, A11;

          hence (f . x) = (f . y) by A2, A12, A13;

        end;

      end;

      now

        let x be Element of X;

        

         A14: r in REAL by XREAL_0:def 1;

        assume x in ( dom f);

        then

         A15: (f . x) = r by A2;

        then -infty < (f . x) by XXREAL_0: 12, A14;

        then

         A16: ( - +infty ) < (f . x) by XXREAL_3:def 3;

        (f . x) < +infty by A15, XXREAL_0: 9, A14;

        hence |.(f . x).| < +infty by A16, EXTREAL1: 22;

      end;

      then f is real-valued by MESFUNC2:def 1;

      hence thesis by A3, MESFUNC2:def 4;

    end;

    theorem :: MESFUNC6:3

    for x be set holds x in ( less_dom (f,a)) iff x in ( dom f) & ex y be Real st y = (f . x) & y < a

    proof

      let x be set;

      (ex y be Real st y = (f . x) & y < a) iff (f . x) < a;

      hence thesis by MESFUNC1:def 11;

    end;

    theorem :: MESFUNC6:4

    for x be set holds x in ( less_eq_dom (f,a)) iff x in ( dom f) & ex y be Real st y = (f . x) & y <= a

    proof

      let x be set;

      (ex y be Real st y = (f . x) & y <= a) iff (f . x) <= a;

      hence thesis by MESFUNC1:def 12;

    end;

    theorem :: MESFUNC6:5

    for x be set holds x in ( great_dom (f,r)) iff x in ( dom f) & ex y be Real st y = (f . x) & r < y

    proof

      let x be set;

      (ex y be Real st y = (f . x) & r < y) iff r < (f . x);

      hence thesis by MESFUNC1:def 13;

    end;

    theorem :: MESFUNC6:6

    for x be set holds x in ( great_eq_dom (f,r)) iff x in ( dom f) & ex y be Real st y = (f . x) & r <= y

    proof

      let x be set;

      (ex y be Real st y = (f . x) & r <= y) iff r <= (f . x);

      hence thesis by MESFUNC1:def 14;

    end;

    theorem :: MESFUNC6:7

    for x be set holds x in ( eq_dom (f,r)) iff x in ( dom f) & ex y be Real st y = (f . x) & r = y

    proof

      let x be set;

      (ex y be Real st y = (f . x) & r = y) iff r = (f . x);

      hence thesis by MESFUNC1:def 15;

    end;

    theorem :: MESFUNC6:8

    (for n holds (F . n) = (Y /\ ( great_dom (f,(r - (1 / (n + 1))))))) implies (Y /\ ( great_eq_dom (f,r))) = ( meet ( rng F))

    proof

      assume for n holds (F . n) = (Y /\ ( great_dom (f,(r - (1 / (n + 1))))));

      then for n be Element of NAT holds (F . n) = (Y /\ ( great_dom (( R_EAL f),(r - (1 / (n + 1))))));

      then (Y /\ ( great_eq_dom (f,r))) = ( meet ( rng F)) by MESFUNC1: 19;

      hence thesis;

    end;

    theorem :: MESFUNC6:9

    (for n holds (F . n) = (Y /\ ( less_dom (f,(r + (1 / (n + 1))))))) implies (Y /\ ( less_eq_dom (f,r))) = ( meet ( rng F))

    proof

      assume for n holds (F . n) = (Y /\ ( less_dom (f,(r + (1 / (n + 1))))));

      then for n be Element of NAT holds (F . n) = (Y /\ ( less_dom (( R_EAL f),(r + (1 / (n + 1))))));

      then (Y /\ ( less_eq_dom (f,r))) = ( meet ( rng F)) by MESFUNC1: 20;

      hence thesis;

    end;

    theorem :: MESFUNC6:10

    (for n holds (F . n) = (Y /\ ( less_eq_dom (f,(r - (1 / (n + 1))))))) implies (Y /\ ( less_dom (f,r))) = ( union ( rng F))

    proof

      assume for n holds (F . n) = (Y /\ ( less_eq_dom (f,(r - (1 / (n + 1))))));

      then for n be Element of NAT holds (F . n) = (Y /\ ( less_eq_dom (( R_EAL f),(r - (1 / (n + 1))))));

      then (Y /\ ( less_dom (f,r))) = ( union ( rng F)) by MESFUNC1: 21;

      hence thesis;

    end;

    theorem :: MESFUNC6:11

    (for n holds (F . n) = (Y /\ ( great_eq_dom (f,(r + (1 / (n + 1))))))) implies (Y /\ ( great_dom (f,r))) = ( union ( rng F))

    proof

      assume for n holds (F . n) = (Y /\ ( great_eq_dom (f,(r + (1 / (n + 1))))));

      then for n be Element of NAT holds (F . n) = (Y /\ ( great_eq_dom (( R_EAL f),(r + (1 / (n + 1))))));

      then (Y /\ ( great_dom (f,r))) = ( union ( rng F)) by MESFUNC1: 22;

      hence thesis;

    end;

    definition

      let X be non empty set;

      let S be SigmaField of X;

      let A be Element of S;

      let f be PartFunc of X, REAL ;

      :: MESFUNC6:def1

      attr f is A -measurable means ( R_EAL f) is A -measurable;

    end

    theorem :: MESFUNC6:12

    

     Th12: f is A -measurable iff for r be Real holds (A /\ ( less_dom (f,r))) in S by MESFUNC1:def 16;

    theorem :: MESFUNC6:13

    

     Th13: A c= ( dom f) implies (f is A -measurable iff for r be Real holds (A /\ ( great_eq_dom (f,r))) in S) by MESFUNC1: 27;

    theorem :: MESFUNC6:14

    f is A -measurable iff for r be Real holds (A /\ ( less_eq_dom (f,r))) in S by MESFUNC1: 28;

    theorem :: MESFUNC6:15

    A c= ( dom f) implies (f is A -measurable iff for r be Real holds (A /\ ( great_dom (f,r))) in S) by MESFUNC1: 29;

    theorem :: MESFUNC6:16

    B c= A & f is A -measurable implies f is B -measurable by MESFUNC1: 30;

    theorem :: MESFUNC6:17

    f is A -measurable & f is B -measurable implies f is (A \/ B) -measurable by MESFUNC1: 31;

    theorem :: MESFUNC6:18

    f is A -measurable & A c= ( dom f) implies ((A /\ ( great_dom (f,r))) /\ ( less_dom (f,s))) in S by MESFUNC1: 32;

    theorem :: MESFUNC6:19

    f is A -measurable & g is A -measurable & A c= ( dom g) implies ((A /\ ( less_dom (f,r))) /\ ( great_dom (g,r))) in S by MESFUNC1: 36;

    theorem :: MESFUNC6:20

    

     Th20: ( R_EAL (r (#) f)) = (r (#) ( R_EAL f))

    proof

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

      then

       A1: ( dom ( R_EAL (r (#) f))) = ( dom (r (#) ( R_EAL f))) by MESFUNC1:def 6;

      now

        let x be object;

        reconsider rr = r as R_eal by XXREAL_0:def 1;

        assume

         A2: x in ( dom ( R_EAL (r (#) f)));

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

        then (( R_EAL (r (#) f)) . x) = (rr * (f . x)) by EXTREAL1: 1;

        hence (( R_EAL (r (#) f)) . x) = ((r (#) ( R_EAL f)) . x) by A1, A2, MESFUNC1:def 6;

      end;

      hence thesis by A1, FUNCT_1: 2;

    end;

    theorem :: MESFUNC6:21

    

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

    proof

      assume that

       A1: f is A -measurable and

       A2: A c= ( dom f);

      ( R_EAL f) is A -measurable by A1;

      then (r (#) ( R_EAL f)) is A -measurable by A2, MESFUNC1: 37;

      then ( R_EAL (r (#) f)) is A -measurable by Th20;

      hence thesis;

    end;

    begin

    reserve X for non empty set,

S for SigmaField of X,

f,g for PartFunc of X, REAL ,

A for Element of S,

r for Real,

p for Rational;

    theorem :: MESFUNC6:22

    ( R_EAL f) is real-valued;

    theorem :: MESFUNC6:23

    

     Th23: ( R_EAL (f + g)) = (( R_EAL f) + ( R_EAL g)) & ( R_EAL (f - g)) = (( R_EAL f) - ( R_EAL g)) & ( dom ( R_EAL (f + g))) = (( dom ( R_EAL f)) /\ ( dom ( R_EAL g))) & ( dom ( R_EAL (f - g))) = (( dom ( R_EAL f)) /\ ( dom ( R_EAL g))) & ( dom ( R_EAL (f + g))) = (( dom f) /\ ( dom g)) & ( dom ( R_EAL (f - g))) = (( dom f) /\ ( dom g))

    proof

      ( dom (( R_EAL f) - ( R_EAL g))) = (( dom ( R_EAL f)) /\ ( dom ( R_EAL g))) by MESFUNC2: 2;

      then

       A1: ( dom (( R_EAL f) - ( R_EAL g))) = ( dom (f - g)) by VALUED_1: 12;

       A2:

      now

        let x be object;

        assume

         A3: x in ( dom (( R_EAL f) - ( R_EAL g)));

        

        then ((( R_EAL f) - ( R_EAL g)) . x) = ((( R_EAL f) . x) - (( R_EAL g) . x)) by MESFUNC1:def 4

        .= ((f . x) - (g . x)) by SUPINF_2: 3;

        hence ((( R_EAL f) - ( R_EAL g)) . x) = ((f - g) . x) by A1, A3, VALUED_1: 13;

      end;

      ( dom (( R_EAL f) + ( R_EAL g))) = (( dom ( R_EAL f)) /\ ( dom ( R_EAL g))) by MESFUNC2: 2;

      then

       A4: ( dom (( R_EAL f) + ( R_EAL g))) = ( dom (f + g)) by VALUED_1:def 1;

      now

        let x be object;

        assume

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

        

        then ((( R_EAL f) + ( R_EAL g)) . x) = ((( R_EAL f) . x) + (( R_EAL g) . x)) by MESFUNC1:def 3

        .= ((f . x) + (g . x)) by SUPINF_2: 1;

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

      end;

      hence thesis by A4, A1, A2, FUNCT_1: 2, MESFUNC2: 2;

    end;

    theorem :: MESFUNC6:24

    for F be Function of RAT , S st (for p holds (F . p) = ((A /\ ( less_dom (f,p))) /\ (A /\ ( less_dom (g,(r - p)))))) holds (A /\ ( less_dom ((f + g),r))) = ( union ( rng F))

    proof

      let F be Function of RAT , S;

      assume for p holds (F . p) = ((A /\ ( less_dom (f,p))) /\ (A /\ ( less_dom (g,(r - p)))));

      then for p holds (F . p) = ((A /\ ( less_dom (( R_EAL f),p))) /\ (A /\ ( less_dom (( R_EAL g),(r - p)))));

      then

       A1: (A /\ ( less_dom ((( R_EAL f) + ( R_EAL g)),r))) = ( union ( rng F)) by MESFUNC2: 3;

      (( R_EAL f) + ( R_EAL g)) = ( R_EAL (f + g)) by Th23;

      hence thesis by A1;

    end;

    theorem :: MESFUNC6:25

    f is A -measurable & g is A -measurable implies ex F be Function of RAT , S st for p be Rational holds (F . p) = ((A /\ ( less_dom (f,p))) /\ (A /\ ( less_dom (g,(r - p))))) by MESFUNC2: 6;

    theorem :: MESFUNC6:26

    

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

    proof

      assume f is A -measurable & g is A -measurable;

      then ( R_EAL f) is A -measurable & ( R_EAL g) is A -measurable;

      then (( R_EAL f) + ( R_EAL g)) is A -measurable by MESFUNC2: 7;

      then ( R_EAL (f + g)) is A -measurable by Th23;

      hence thesis;

    end;

    theorem :: MESFUNC6:27

    (( R_EAL f) - ( R_EAL g)) = (( R_EAL f) + ( R_EAL ( - g)))

    proof

      (( R_EAL f) - ( R_EAL g)) = ( R_EAL (f - g)) by Th23

      .= ( R_EAL (f + ( - g)));

      hence thesis by Th23;

    end;

    theorem :: MESFUNC6:28

    

     Th28: ( - ( R_EAL f)) = ( R_EAL (( - 1) (#) f)) & ( - ( R_EAL f)) = ( R_EAL ( - f))

    proof

      ( - ( R_EAL f)) = (( - 1) (#) ( R_EAL f)) by MESFUNC2: 9;

      hence thesis by Th20;

    end;

    theorem :: MESFUNC6:29

    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);

      ( R_EAL g) is A -measurable by A2;

      then (( - 1) (#) ( R_EAL g)) is A -measurable by A3, MESFUNC1: 37;

      then ( - ( R_EAL g)) is A -measurable by MESFUNC2: 9;

      then

       A4: ( R_EAL ( - g)) is A -measurable by Th28;

      ( R_EAL f) is A -measurable by A1;

      then (( R_EAL f) + ( R_EAL ( - g))) is A -measurable by A4, MESFUNC2: 7;

      then ( R_EAL (f - g)) is A -measurable by Th23;

      hence thesis;

    end;

    begin

    reserve X for non empty set,

f,g for PartFunc of X, REAL ,

r for Real;

    theorem :: MESFUNC6:30

    

     Th30: ( max+ ( R_EAL f)) = ( max+ f) & ( max- ( R_EAL f)) = ( max- f)

    proof

      

       A1: ( dom ( max+ ( R_EAL f))) = ( dom ( R_EAL f)) by MESFUNC2:def 2

      .= ( dom ( max+ f)) by RFUNCT_3:def 10;

      now

        let x be object;

        assume

         A2: x in ( dom ( max+ ( R_EAL f)));

        then (( max+ ( R_EAL f)) . x) = ( max+ (f . x)) by MESFUNC2:def 2;

        hence (( max+ ( R_EAL f)) . x) = (( max+ f) . x) by A1, A2, RFUNCT_3:def 10;

      end;

      hence ( max+ ( R_EAL f)) = ( max+ f) by A1, FUNCT_1: 2;

      

       A3: ( dom ( max- ( R_EAL f))) = ( dom ( R_EAL f)) by MESFUNC2:def 3

      .= ( dom ( max- f)) by RFUNCT_3:def 11;

      now

        let x be object;

        assume

         A4: x in ( dom ( max- ( R_EAL f)));

        (( max- ( R_EAL f)) . x) = ( max (( - (( R_EAL f) . x)), 0. )) by MESFUNC2:def 3, A4;

        then (( max- ( R_EAL f)) . x) = ( max- (f . x)) by SUPINF_2: 2;

        hence (( max- ( R_EAL f)) . x) = (( max- f) . x) by A3, A4, RFUNCT_3:def 11;

      end;

      hence thesis by A3, FUNCT_1: 2;

    end;

    theorem :: MESFUNC6:31

    for x be Element of X holds 0 <= (( max+ f) . x)

    proof

      let x be Element of X;

       0. <= (( max+ ( R_EAL f)) . x) by MESFUNC2: 12;

      hence thesis by Th30;

    end;

    theorem :: MESFUNC6:32

    for x be Element of X holds 0 <= (( max- f) . x)

    proof

      let x be Element of X;

       0. <= (( max- ( R_EAL f)) . x) by MESFUNC2: 13;

      hence thesis by Th30;

    end;

    theorem :: MESFUNC6:33

    ( max- f) = ( max+ ( - f))

    proof

      ( max- f) = ( max- ( R_EAL f)) by Th30;

      then ( max- f) = ( max+ ( - ( R_EAL f))) by MESFUNC2: 14;

      then ( max- f) = ( max+ ( R_EAL ( - f))) by Th28;

      hence thesis by Th30;

    end;

    theorem :: MESFUNC6:34

    for x be set st x in ( dom f) & 0 < (( max+ f) . x) holds (( max- f) . x) = 0

    proof

      let x be set;

      assume that

       A1: x in ( dom f) and

       A2: 0 < (( max+ f) . x);

       0. < (( max+ ( R_EAL f)) . x) by A2, Th30;

      then (( max- ( R_EAL f)) . x) = 0. by A1, MESFUNC2: 15;

      hence thesis by Th30;

    end;

    theorem :: MESFUNC6:35

    for x be set st x in ( dom f) & 0 < (( max- f) . x) holds (( max+ f) . x) = 0

    proof

      let x be set;

      assume that

       A1: x in ( dom f) and

       A2: 0 < (( max- f) . x);

       0. < (( max- ( R_EAL f)) . x) by A2, Th30;

      then (( max+ ( R_EAL f)) . x) = 0. by A1, MESFUNC2: 16;

      hence thesis by Th30;

    end;

    theorem :: MESFUNC6:36

    ( dom f) = ( dom (( max+ f) - ( max- f))) & ( dom f) = ( dom (( max+ f) + ( max- f)))

    proof

      ( dom f) = ( dom (( max+ ( R_EAL f)) - ( max- ( R_EAL f)))) by MESFUNC2: 17;

      then ( dom f) = ( dom (( R_EAL ( max+ f)) - ( max- ( R_EAL f)))) by Th30;

      then ( dom f) = ( dom (( R_EAL ( max+ f)) - ( R_EAL ( max- f)))) by Th30;

      then ( dom f) = ( dom ( R_EAL (( max+ f) - ( max- f)))) by Th23;

      hence ( dom f) = ( dom (( max+ f) - ( max- f)));

      ( dom f) = ( dom (( max+ ( R_EAL f)) + ( max- ( R_EAL f)))) by MESFUNC2: 17;

      then ( dom f) = ( dom (( R_EAL ( max+ f)) + ( max- ( R_EAL f)))) by Th30;

      then ( dom f) = ( dom (( R_EAL ( max+ f)) + ( R_EAL ( max- f)))) by Th30;

      then ( dom f) = ( dom ( R_EAL (( max+ f) + ( max- f)))) by Th23;

      hence thesis;

    end;

    theorem :: MESFUNC6:37

    for x be set st x in ( dom f) holds ((( max+ f) . x) = (f . x) or (( max+ f) . x) = 0 ) & ((( max- f) . x) = ( - (f . x)) or (( max- f) . x) = 0 )

    proof

      let x be set;

      assume

       A1: x in ( dom f);

      then (( max+ ( R_EAL f)) . x) = (( R_EAL f) . x) or (( max+ ( R_EAL f)) . x) = 0. by MESFUNC2: 18;

      hence (( max+ f) . x) = (f . x) or (( max+ f) . x) = 0 by Th30;

      (( max- ( R_EAL f)) . x) = ( - (( R_EAL f) . x)) or (( max- ( R_EAL f)) . x) = 0. by A1, MESFUNC2: 18;

      hence thesis by Th30;

    end;

    theorem :: MESFUNC6:38

    for x be set st x in ( dom f) & (( max+ f) . x) = (f . x) holds (( max- f) . x) = 0

    proof

      let x be set;

      assume that

       A1: x in ( dom f) and

       A2: (( max+ f) . x) = (f . x);

      (f . x) = (( max+ ( R_EAL f)) . x) by A2, Th30;

      then (( max- ( R_EAL f)) . x) = 0. by A1, MESFUNC2: 19;

      hence thesis by Th30;

    end;

    theorem :: MESFUNC6:39

    for x be set st x in ( dom f) & (( max+ f) . x) = 0 holds (( max- f) . x) = ( - (f . x))

    proof

      let x be set;

      assume that

       A1: x in ( dom f) and

       A2: (( max+ f) . x) = 0 ;

       0 = (( max+ ( R_EAL f)) . x) by A2, Th30;

      then (( max- ( R_EAL f)) . x) = ( - (( R_EAL f) . x)) by A1, MESFUNC2: 20;

      then (( max- f) . x) = ( - (( R_EAL f) . x)) by Th30;

      hence thesis;

    end;

    theorem :: MESFUNC6:40

    for x be set st x in ( dom f) & (( max- f) . x) = ( - (f . x)) holds (( max+ f) . x) = 0

    proof

      let x be set;

      assume that

       A1: x in ( dom f) and

       A2: (( max- f) . x) = ( - (f . x));

      ( - (f . x)) = (( max- ( R_EAL f)) . x) by A2, Th30;

      then ( - (( R_EAL f) . x)) = (( max- ( R_EAL f)) . x);

      then (( max+ ( R_EAL f)) . x) = 0. by A1, MESFUNC2: 21;

      hence thesis by Th30;

    end;

    theorem :: MESFUNC6:41

    for x be set st x in ( dom f) & (( max- f) . x) = 0 holds (( max+ f) . x) = (f . x)

    proof

      let x be set;

      assume that

       A1: x in ( dom f) and

       A2: (( max- f) . x) = 0 ;

       0 = (( max- ( R_EAL f)) . x) by A2, Th30;

      then (( max+ ( R_EAL f)) . x) = (( R_EAL f) . x) by A1, MESFUNC2: 22;

      hence thesis by Th30;

    end;

    theorem :: MESFUNC6:42

    f = (( max+ f) - ( max- f))

    proof

      f = (( max+ ( R_EAL f)) - ( max- ( R_EAL f))) by MESFUNC2: 23;

      then f = (( R_EAL ( max+ f)) - ( max- ( R_EAL f))) by Th30;

      then f = (( R_EAL ( max+ f)) - ( R_EAL ( max- f))) by Th30;

      then f = ( R_EAL (( max+ f) - ( max- f))) by Th23;

      hence thesis;

    end;

    theorem :: MESFUNC6:43

    

     Th43: |.r qua Complex.| = |.r.|

    proof

      reconsider rr = r as Real;

      per cases ;

        suppose

         A1: 0 <= r;

        then |.r.| = r by EXTREAL1:def 1;

        hence thesis by A1, ABSVALUE:def 1;

      end;

        suppose

         A2: r < 0 ;

        then |.r.| = ( - r qua ExtReal) by EXTREAL1:def 1;

        then |.rr.| = ( - rr);

        hence thesis by A2, ABSVALUE:def 1;

      end;

    end;

    theorem :: MESFUNC6:44

    

     Th44: ( R_EAL ( abs f)) = |.( R_EAL f).|

    proof

      

       A1: ( dom ( R_EAL ( abs f))) = ( dom f) by VALUED_1:def 11

      .= ( dom |.( R_EAL f).|) by MESFUNC1:def 10;

      now

        let x be object;

        reconsider fx = (f . x) as Real;

        (( R_EAL ( abs f)) . x) = |.fx qua Complex.| by VALUED_1: 18;

        then

         A2: (( R_EAL ( abs f)) . x) = |.(f . x).| by Th43;

        assume x in ( dom ( R_EAL ( abs f)));

        hence (( R_EAL ( abs f)) . x) = ( |.( R_EAL f).| . x) by A1, A2, MESFUNC1:def 10;

      end;

      hence thesis by A1, FUNCT_1: 2;

    end;

    theorem :: MESFUNC6:45

    ( abs f) = (( max+ f) + ( max- f))

    proof

      ( abs f) = ( R_EAL ( abs f));

      then ( abs f) = |.( R_EAL f).| by Th44;

      then ( abs f) = (( max+ ( R_EAL f)) + ( max- ( R_EAL f))) by MESFUNC2: 24;

      then ( abs f) = (( R_EAL ( max+ f)) + ( max- ( R_EAL f))) by Th30;

      then ( abs f) = (( R_EAL ( max+ f)) + ( R_EAL ( max- f))) by Th30;

      then ( abs f) = ( R_EAL (( max+ f) + ( max- f))) by Th23;

      hence thesis;

    end;

    begin

    reserve X for non empty set,

S for SigmaField of X,

f,g for PartFunc of X, REAL ,

A for Element of S;

    theorem :: MESFUNC6:46

    

     Th46: f is A -measurable implies ( max+ f) is A -measurable

    proof

      assume f is A -measurable;

      then ( R_EAL f) is A -measurable;

      then ( max+ ( R_EAL f)) is A -measurable by MESFUNC2: 25;

      then ( R_EAL ( max+ f)) is A -measurable by Th30;

      hence thesis;

    end;

    theorem :: MESFUNC6:47

    

     Th47: f is A -measurable & A c= ( dom f) implies ( max- f) is A -measurable

    proof

      assume that

       A1: f is A -measurable and

       A2: A c= ( dom f);

      ( R_EAL f) is A -measurable by A1;

      then ( max- ( R_EAL f)) is A -measurable by A2, MESFUNC2: 26;

      then ( R_EAL ( max- f)) is A -measurable by Th30;

      hence thesis;

    end;

    theorem :: MESFUNC6:48

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

    proof

      assume that

       A1: f is A -measurable and

       A2: A c= ( dom f);

      ( R_EAL f) is A -measurable by A1;

      then |.( R_EAL f).| is A -measurable by A2, MESFUNC2: 27;

      then ( R_EAL ( abs f)) is A -measurable by Th44;

      hence thesis;

    end;

    begin

    reserve X for non empty set,

Y for set,

S for SigmaField of X,

f,g,h for PartFunc of X, REAL ,

A for Element of S,

r for Real;

    definition

      let X, S, f;

      :: MESFUNC6:def2

      pred f is_simple_func_in S means ex F be Finite_Sep_Sequence of S st (( dom f) = ( union ( rng F)) & for n be Nat, x,y be Element of X st n in ( dom F) & x in (F . n) & y in (F . n) holds (f . x) = (f . y));

    end

    theorem :: MESFUNC6:49

    

     Th49: f is_simple_func_in S iff ( R_EAL f) is_simple_func_in S by MESFUNC2:def 4;

    theorem :: MESFUNC6:50

    f is_simple_func_in S implies f is A -measurable by Th49, MESFUNC2: 34;

    theorem :: MESFUNC6:51

    

     Th51: for X be set, f be PartFunc of X, REAL holds f is nonnegative iff for x be object holds 0 <= (f . x)

    proof

      let X be set, f be PartFunc of X, REAL ;

      hereby

        assume f is nonnegative;

        then

         A1: ( rng f) is nonnegative;

        hereby

          let x be object;

          now

            assume x in ( dom f);

            then

             A2: (f . x) in ( rng f) by FUNCT_1:def 3;

            thus 0 <= (f . x) by A1, A2;

          end;

          hence 0 <= (f . x) by FUNCT_1:def 2;

        end;

      end;

      assume

       A3: for x be object holds 0 <= (f . x);

      let y be ExtReal;

      assume y in ( rng f);

      then ex x be object st x in ( dom f) & y = (f . x) by FUNCT_1:def 3;

      hence thesis by A3;

    end;

    theorem :: MESFUNC6:52

    

     Th52: for X be set, f be PartFunc of X, REAL st for x be object st x in ( dom f) holds 0 <= (f . x) holds f is nonnegative

    proof

      let X be set, f be PartFunc of X, REAL such that

       A1: for x be object st x in ( dom f) holds 0 <= (f . x);

      let y be ExtReal;

      assume y in ( rng f);

      then ex x be object st x in ( dom f) & y = (f . x) by FUNCT_1:def 3;

      hence thesis by A1;

    end;

    theorem :: MESFUNC6:53

    for X be set, f be PartFunc of X, REAL holds f is nonpositive iff for x be set holds (f . x) <= 0

    proof

      let X be set, f be PartFunc of X, REAL ;

      hereby

        assume f is nonpositive;

        then

         A1: ( rng f) is nonpositive;

        hereby

          let x be set;

          now

            assume x in ( dom f);

            then

             A2: (f . x) in ( rng f) by FUNCT_1:def 3;

            thus (f . x) <= 0 by A1, A2;

          end;

          hence (f . x) <= 0 by FUNCT_1:def 2;

        end;

      end;

      assume

       A3: for x be set holds (f . x) <= 0 ;

      let y be R_eal;

      assume y in ( rng f);

      then ex x be object st x in ( dom f) & y = (f . x) by FUNCT_1:def 3;

      hence thesis by A3;

    end;

    theorem :: MESFUNC6:54

    

     Th54: (for x be object st x in ( dom f) holds (f . x) <= 0 ) implies f is nonpositive

    proof

      assume

       A1: for x be object st x in ( dom f) holds (f . x) <= 0 ;

      let y be R_eal;

      assume y in ( rng f);

      then ex x be object st x in ( dom f) & y = (f . x) by FUNCT_1:def 3;

      hence thesis by A1;

    end;

    theorem :: MESFUNC6:55

    f is nonnegative implies (f | Y) is nonnegative

    proof

      assume f is nonnegative;

      then

       A1: ( rng f) is nonnegative;

      now

        let y be ExtReal;

        assume y in ( rng (f | Y));

        then

        consider x be object such that

         A2: x in ( dom (f | Y)) and

         A3: ((f | Y) . x) = y by FUNCT_1:def 3;

        x in (( dom f) /\ Y) by A2, RELAT_1: 61;

        then

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

        ((f | Y) . x) = (f . x) by A2, FUNCT_1: 47;

        then ((f | Y) . x) in ( rng f) by A4, FUNCT_1: 3;

        hence 0. <= y by A1, A3;

      end;

      then ( rng (f | Y)) is nonnegative;

      hence thesis;

    end;

    theorem :: MESFUNC6:56

    

     Th56: f is nonnegative & g is nonnegative implies (f + g) is nonnegative

    proof

      assume that

       A1: f is nonnegative and

       A2: g is nonnegative;

      for x be object st x in ( dom (f + g)) holds 0 <= ((f + g) . x)

      proof

        let x be object such that

         A3: x in ( dom (f + g));

         0 <= (f . x) by A1, Th51;

        then

         A4: (g . x) <= ((f . x) + (g . x)) by XREAL_1: 31;

         0 <= (g . x) by A2, Th51;

        hence thesis by A3, A4, VALUED_1:def 1;

      end;

      hence thesis by Th52;

    end;

    theorem :: MESFUNC6:57

    f is nonnegative implies ( 0 <= r implies (r (#) f) is nonnegative) & (r <= 0 implies (r (#) f) is nonpositive)

    proof

      assume

       A1: f is nonnegative;

      hereby

        assume

         A2: 0 <= r;

        now

          let x be object such that

           A3: x in ( dom (r (#) f));

           0 <= (f . x) by A1, Th51;

          then ( 0 * r) <= (r * (f . x)) by A2;

          hence 0 <= ((r (#) f) . x) by A3, VALUED_1:def 5;

        end;

        hence (r (#) f) is nonnegative by Th52;

      end;

      assume

       A4: r <= 0 ;

      now

        let x be object such that

         A5: x in ( dom (r (#) f));

         0 <= (f . x) by A1, Th51;

        then (r * (f . x)) <= (r * 0 ) by A4;

        hence ((r (#) f) . x) <= 0 by A5, VALUED_1:def 5;

      end;

      hence thesis by Th54;

    end;

    theorem :: MESFUNC6:58

    

     Th58: (for x be set st x in (( dom f) /\ ( dom g)) holds (g . x) <= (f . x)) implies (f - g) is nonnegative

    proof

      assume

       A1: for x be set st x in (( dom f) /\ ( dom g)) holds (g . x) <= (f . x);

      now

        let x be object such that

         A2: x in ( dom (f - g));

        ( dom (f - g)) = (( dom f) /\ ( dom g)) by VALUED_1: 12;

        then 0 <= ((f . x) - (g . x)) by A1, A2, XREAL_1: 48;

        hence 0 <= ((f - g) . x) by A2, VALUED_1: 13;

      end;

      hence thesis by Th52;

    end;

    theorem :: MESFUNC6:59

    f is nonnegative & g is nonnegative & h is nonnegative implies ((f + g) + h) is nonnegative

    proof

      assume that

       A1: f is nonnegative & g is nonnegative and

       A2: h is nonnegative;

      (f + g) is nonnegative by A1, Th56;

      hence thesis by A2, Th56;

    end;

    theorem :: MESFUNC6:60

    

     Th60: for x be object st x in ( dom ((f + g) + h)) holds (((f + g) + h) . x) = (((f . x) + (g . x)) + (h . x))

    proof

      let x be object;

      assume

       A1: x in ( dom ((f + g) + h));

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

      then x in ( dom (f + g)) by A1, XBOOLE_0:def 4;

      then (((f . x) + (g . x)) + (h . x)) = (((f + g) . x) + (h . x)) by VALUED_1:def 1;

      hence thesis by A1, VALUED_1:def 1;

    end;

    theorem :: MESFUNC6:61

    ( max+ f) is nonnegative & ( max- f) is nonnegative

    proof

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

      hence ( max+ f) is nonnegative by Th52;

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

      hence thesis by Th52;

    end;

    theorem :: MESFUNC6:62

    

     Th62: ( dom (( max+ (f + g)) + ( max- f))) = (( dom f) /\ ( dom g)) & ( dom (( max- (f + g)) + ( max+ f))) = (( dom f) /\ ( dom g)) & ( dom ((( max+ (f + g)) + ( max- f)) + ( max- g))) = (( dom f) /\ ( dom g)) & ( dom ((( max- (f + g)) + ( max+ f)) + ( max+ g))) = (( dom f) /\ ( dom g)) & (( max+ (f + g)) + ( max- f)) is nonnegative & (( max- (f + g)) + ( max+ f)) is nonnegative

    proof

      

       A1: ( dom ( max- f)) = ( dom f) & ( dom (( max+ (f + g)) + ( max- f))) = (( dom ( max+ (f + g))) /\ ( dom ( max- f))) by RFUNCT_3:def 11, VALUED_1:def 1;

      

       A2: ( dom ( max+ f)) = ( dom f) & ( dom (( max- (f + g)) + ( max+ f))) = (( dom ( max- (f + g))) /\ ( dom ( max+ f))) by RFUNCT_3:def 10, VALUED_1:def 1;

      

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

      then

       A4: ( dom ( max- (f + g))) = (( dom f) /\ ( dom g)) by RFUNCT_3:def 11;

      ( dom ( max+ (f + g))) = (( dom f) /\ ( dom g)) by A3, RFUNCT_3:def 10;

      then

       A5: ( dom (( max+ (f + g)) + ( max- f))) = (( dom g) /\ (( dom f) /\ ( dom f))) by A1, XBOOLE_1: 16;

      hence ( dom (( max+ (f + g)) + ( max- f))) = (( dom f) /\ ( dom g)) & ( dom (( max- (f + g)) + ( max+ f))) = (( dom f) /\ ( dom g)) by A4, A2, XBOOLE_1: 16;

      ( dom ( max- g)) = ( dom g) by RFUNCT_3:def 11;

      

      then ( dom ((( max+ (f + g)) + ( max- f)) + ( max- g))) = ((( dom f) /\ ( dom g)) /\ ( dom g)) by A5, VALUED_1:def 1

      .= (( dom f) /\ (( dom g) /\ ( dom g))) by XBOOLE_1: 16;

      hence ( dom ((( max+ (f + g)) + ( max- f)) + ( max- g))) = (( dom f) /\ ( dom g));

      ( dom ( max+ g)) = ( dom g) & ( dom (( max- (f + g)) + ( max+ f))) = (( dom g) /\ (( dom f) /\ ( dom f))) by A4, A2, RFUNCT_3:def 10, XBOOLE_1: 16;

      then ( dom ((( max- (f + g)) + ( max+ f)) + ( max+ g))) = ((( dom f) /\ ( dom g)) /\ ( dom g)) by VALUED_1:def 1;

      then ( dom ((( max- (f + g)) + ( max+ f)) + ( max+ g))) = (( dom f) /\ (( dom g) /\ ( dom g))) by XBOOLE_1: 16;

      hence ( dom ((( max- (f + g)) + ( max+ f)) + ( max+ g))) = (( dom f) /\ ( dom g));

      now

        let x be object;

        assume

         A6: x in ( dom (( max+ (f + g)) + ( max- f)));

        then 0 <= (( max+ (f + g)) . x) & 0 <= (( max- f) . x) by RFUNCT_3: 37, RFUNCT_3: 40;

        then ( 0 + 0 ) <= ((( max+ (f + g)) . x) + (( max- f) . x));

        hence 0 <= ((( max+ (f + g)) + ( max- f)) . x) by A6, VALUED_1:def 1;

      end;

      hence (( max+ (f + g)) + ( max- f)) is nonnegative by Th52;

      now

        let x be object;

        assume

         A7: x in ( dom (( max- (f + g)) + ( max+ f)));

        then 0 <= (( max- (f + g)) . x) & 0 <= (( max+ f) . x) by RFUNCT_3: 37, RFUNCT_3: 40;

        then ( 0 + 0 ) <= ((( max- (f + g)) . x) + (( max+ f) . x));

        hence 0 <= ((( max- (f + g)) + ( max+ f)) . x) by A7, VALUED_1:def 1;

      end;

      hence thesis by Th52;

    end;

    theorem :: MESFUNC6:63

    ((( max+ (f + g)) + ( max- f)) + ( max- g)) = ((( max- (f + g)) + ( max+ f)) + ( max+ g))

    proof

      

       A1: ( dom ( max+ (f + g))) = ( dom (f + g)) by RFUNCT_3:def 10;

      

       A2: ( dom ( max+ g)) = ( dom g) by RFUNCT_3:def 10;

      

       A3: ( dom ( max+ f)) = ( dom f) by RFUNCT_3:def 10;

      

       A4: ( dom ( max- f)) = ( dom f) by RFUNCT_3:def 11;

      

       A5: ( dom ( max- g)) = ( dom g) by RFUNCT_3:def 11;

      

       A6: ( dom ((( max+ (f + g)) + ( max- f)) + ( max- g))) = (( dom (( max+ (f + g)) + ( max- f))) /\ ( dom ( max- g))) by VALUED_1:def 1

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

      then

       A7: ( dom ((( max+ (f + g)) + ( max- f)) + ( max- g))) = (( dom (f + g)) /\ (( dom f) /\ ( dom g))) by XBOOLE_1: 16;

      

       A8: ( dom ( max- (f + g))) = ( dom (f + g)) by RFUNCT_3:def 11;

      

       A9: for x be object st x in ( dom ((( max+ (f + g)) + ( max- f)) + ( max- g))) holds (((( max+ (f + g)) + ( max- f)) + ( max- g)) . x) = (((( max- (f + g)) + ( max+ f)) + ( max+ g)) . x)

      proof

        let x be object;

        assume

         A10: x in ( dom ((( max+ (f + g)) + ( max- f)) + ( max- g)));

        then

         A11: x in ( dom g) by A6, XBOOLE_0:def 4;

        then

         A12: (( max+ g) . x) = ( max+ (g . x)) by A2, RFUNCT_3:def 10;

        

         A13: (( max- g) . x) = ( max- (g . x)) by A5, A11, RFUNCT_3:def 11;

        

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

        

        then

         A15: (( max+ (f + g)) . x) = ( max+ ((f + g) . x)) by A1, A7, A10, RFUNCT_3:def 10

        .= ( max (((f . x) + (g . x)), 0 )) by A7, A10, A14, VALUED_1:def 1;

        

         A16: x in ( dom f) by A7, A10, A14, XBOOLE_0:def 4;

        then

         A17: (( max+ f) . x) = ( max+ (f . x)) by A3, RFUNCT_3:def 10;

        

         A18: (( max- (f + g)) . x) = ( max- ((f + g) . x)) by A8, A7, A10, A14, RFUNCT_3:def 11

        .= ( max (( - ((f . x) + (g . x))), 0 )) by A7, A10, A14, VALUED_1:def 1;

        

         A19: (( max- f) . x) = ( max- (f . x)) by A4, A16, RFUNCT_3:def 11;

         A20:

        now

          assume

           A21: 0 <= (f . x);

          then

           A22: (( max- f) . x) = 0 by A19, XXREAL_0:def 10;

           A23:

          now

            assume

             A24: (g . x) < 0 ;

            then

             A25: (( max- g) . x) = ( - (g . x)) by A13, XXREAL_0:def 10;

            

             A26: (( max+ g) . x) = 0 by A12, A24, XXREAL_0:def 10;

             A27:

            now

              assume

               A28: ((f . x) + (g . x)) < 0 ;

              then (( max- (f + g)) . x) = ( - ((f . x) + (g . x))) by A18, XXREAL_0:def 10;

              then (((( max- (f + g)) . x) + (( max+ f) . x)) + (( max+ g) . x)) = ((( - ((f . x) + (g . x) qua Real)) + (f . x)) + 0 ) by A17, A21, A26, XXREAL_0:def 10;

              hence (((( max+ (f + g)) . x) + (( max- f) . x)) + (( max- g) . x)) = (((( max- (f + g)) . x) + (( max+ f) . x)) + (( max+ g) . x)) by A15, A22, A25, A28, XXREAL_0:def 10;

            end;

            now

              assume 0 <= ((f . x) + (g . x));

              then (( max- (f + g)) . x) = 0 & (((( max+ (f + g)) . x) + (( max- f) . x)) + (( max- g) . x)) = ((((f . x) + (g . x) qua Real) + 0 ) + ( - (g . x) qua Real)) by A15, A18, A22, A25, XXREAL_0:def 10;

              hence (((( max+ (f + g)) . x) + (( max- f) . x)) + (( max- g) . x)) = (((( max- (f + g)) . x) + (( max+ f) . x)) + (( max+ g) . x)) by A17, A21, A26, XXREAL_0:def 10;

            end;

            hence (((( max+ (f + g)) . x) + (( max- f) . x)) + (( max- g) . x)) = (((( max- (f + g)) . x) + (( max+ f) . x)) + (( max+ g) . x)) by A27;

          end;

          now

            assume

             A29: 0 <= (g . x);

            then (( max- g) . x) = 0 by A13, XXREAL_0:def 10;

            then

             A30: (((( max+ (f + g)) . x) + (( max- f) . x)) + (( max- g) . x)) = ((f . x) + (g . x)) by A15, A21, A22, A29, XXREAL_0:def 10;

            (( max- (f + g)) . x) = 0 & (( max+ g) . x) = (g . x) by A18, A12, A21, A29, XXREAL_0:def 10;

            hence (((( max+ (f + g)) . x) + (( max- f) . x)) + (( max- g) . x)) = (((( max- (f + g)) . x) + (( max+ f) . x)) + (( max+ g) . x)) by A17, A21, A30, XXREAL_0:def 10;

          end;

          hence (((( max+ (f + g)) . x) + (( max- f) . x)) + (( max- g) . x)) = (((( max- (f + g)) . x) + (( max+ f) . x)) + (( max+ g) . x)) by A23;

        end;

         A31:

        now

          assume

           A32: (f . x) < 0 ;

          then

           A33: (( max- f) . x) = ( - (f . x)) by A19, XXREAL_0:def 10;

           A34:

          now

            assume

             A35: 0 <= (g . x);

            then

             A36: (( max- g) . x) = 0 by A13, XXREAL_0:def 10;

            

             A37: (( max+ g) . x) = (g . x) by A12, A35, XXREAL_0:def 10;

             A38:

            now

              assume

               A39: ((f . x) + (g . x)) < 0 ;

              then (( max- (f + g)) . x) = ( - ((f . x) + (g . x))) by A18, XXREAL_0:def 10;

              

              then (((( max- (f + g)) . x) + (( max+ f) . x)) + (( max+ g) . x)) = ((( - ((f . x) + (g . x) qua Real)) + 0 ) + (g . x)) by A17, A32, A37, XXREAL_0:def 10

              .= (( - (f . x)) + (( - (g . x)) + (g . x)));

              hence (((( max+ (f + g)) . x) + (( max- f) . x)) + (( max- g) . x)) = (((( max- (f + g)) . x) + (( max+ f) . x)) + (( max+ g) . x)) by A15, A33, A36, A39, XXREAL_0:def 10;

            end;

            now

              assume 0 <= ((f . x) + (g . x));

              then (( max- (f + g)) . x) = 0 & (((( max+ (f + g)) . x) + (( max- f) . x)) + (( max- g) . x)) = ((((f . x) + (g . x) qua Real) + ( - (f . x) qua Real)) + 0 ) by A15, A18, A33, A36, XXREAL_0:def 10;

              hence (((( max+ (f + g)) . x) + (( max- f) . x)) + (( max- g) . x)) = (((( max- (f + g)) . x) + (( max+ f) . x)) + (( max+ g) . x)) by A17, A32, A37, XXREAL_0:def 10;

            end;

            hence (((( max+ (f + g)) . x) + (( max- f) . x)) + (( max- g) . x)) = (((( max- (f + g)) . x) + (( max+ f) . x)) + (( max+ g) . x)) by A38;

          end;

          now

            assume

             A40: (g . x) < 0 ;

            then (( max- (f + g)) . x) = ( - ((f . x) + (g . x))) & (( max+ g) . x) = 0 by A18, A12, A32, XXREAL_0:def 10;

            then

             A41: (((( max- (f + g)) . x) + (( max+ f) . x)) + (( max+ g) . x)) = ((( - ((f . x) + (g . x) qua Real)) + 0 ) + 0 ) by A17, A32, XXREAL_0:def 10;

            (( max- g) . x) = ( - (g . x)) by A13, A40, XXREAL_0:def 10;

            then (((( max+ (f + g)) . x) + (( max- f) . x)) + (( max- g) . x)) = (( 0 + ( - (f . x) qua Real)) + ( - (g . x) qua Real)) by A15, A32, A33, A40, XXREAL_0:def 10;

            hence (((( max+ (f + g)) . x) + (( max- f) . x)) + (( max- g) . x)) = (((( max- (f + g)) . x) + (( max+ f) . x)) + (( max+ g) . x)) by A41;

          end;

          hence (((( max+ (f + g)) . x) + (( max- f) . x)) + (( max- g) . x)) = (((( max- (f + g)) . x) + (( max+ f) . x)) + (( max+ g) . x)) by A34;

        end;

        x in (( dom f) /\ ( dom g)) by A10, Th62;

        then x in ( dom ((( max- (f + g)) + ( max+ f)) + ( max+ g))) by Th62;

        then (((( max- (f + g)) + ( max+ f)) + ( max+ g)) . x) = (((( max- (f + g)) . x) + (( max+ f) . x)) + (( max+ g) . x)) by Th60;

        hence thesis by A10, A20, A31, Th60;

      end;

      ( dom ((( max+ (f + g)) + ( max- f)) + ( max- g))) = (( dom f) /\ ( dom g)) by Th62;

      then ( dom ((( max+ (f + g)) + ( max- f)) + ( max- g))) = ( dom ((( max- (f + g)) + ( max+ f)) + ( max+ g))) by Th62;

      hence thesis by A9, FUNCT_1: 2;

    end;

    theorem :: MESFUNC6:64

     0 <= r implies ( max+ (r (#) f)) = (r (#) ( max+ f)) & ( max- (r (#) f)) = (r (#) ( max- f))

    proof

      assume

       A1: 0 <= r;

      

       A2: ( dom ( max+ (r (#) f))) = ( dom (r (#) f)) by RFUNCT_3:def 10

      .= ( dom f) by VALUED_1:def 5

      .= ( dom ( max+ f)) by RFUNCT_3:def 10

      .= ( dom (r (#) ( max+ f))) by VALUED_1:def 5;

      reconsider rr = r as Real;

      for x be Element of X st x in ( dom ( max+ (r (#) f))) holds (( max+ (r (#) f)) . x) = ((r (#) ( max+ f)) . x)

      proof

        let x be Element of X;

        assume

         A3: x in ( dom ( max+ (r (#) f)));

        then

         A4: x in ( dom (r (#) f)) by RFUNCT_3:def 10;

        then x in ( dom f) by VALUED_1:def 5;

        then

         A5: x in ( dom ( max+ f)) by RFUNCT_3:def 10;

        

         A6: (( max+ (r (#) f)) . x) = ( max+ ((r (#) f) . x)) by A3, RFUNCT_3:def 10

        .= ( max ((r * (f . x)), 0 )) by A4, VALUED_1:def 5;

        ((r (#) ( max+ f)) . x) = (r * (( max+ f) . x)) by A2, A3, VALUED_1:def 5

        .= (rr * ( max+ (f . x))) by A5, RFUNCT_3:def 10

        .= ( max ((rr * (f . x)),(rr * 0 ))) by A1, FUZZY_2: 41;

        hence thesis by A6;

      end;

      hence ( max+ (r (#) f)) = (r (#) ( max+ f)) by A2, PARTFUN1: 5;

      

       A7: ( dom ( max- (r (#) f))) = ( dom (r (#) f)) by RFUNCT_3:def 11

      .= ( dom f) by VALUED_1:def 5

      .= ( dom ( max- f)) by RFUNCT_3:def 11

      .= ( dom (r (#) ( max- f))) by VALUED_1:def 5;

      for x be Element of X st x in ( dom ( max- (r (#) f))) holds (( max- (r (#) f)) . x) = ((r (#) ( max- f)) . x)

      proof

        let x be Element of X;

        assume

         A8: x in ( dom ( max- (r (#) f)));

        then

         A9: x in ( dom (r (#) f)) by RFUNCT_3:def 11;

        then x in ( dom f) by VALUED_1:def 5;

        then

         A10: x in ( dom ( max- f)) by RFUNCT_3:def 11;

        

         A11: (( max- (r (#) f)) . x) = ( max- ((r (#) f) . x)) by A8, RFUNCT_3:def 11

        .= ( max (( - (r * (f . x))), 0 )) by A9, VALUED_1:def 5;

        ((r (#) ( max- f)) . x) = (r * (( max- f) . x)) by A7, A8, VALUED_1:def 5

        .= (rr * ( max- (f . x))) by A10, RFUNCT_3:def 11

        .= ( max ((rr * ( - (f . x) qua Real) qua Real),(rr * 0 ))) by A1, FUZZY_2: 41

        .= ( max (( - (r * (f . x))),(r * 0 )));

        hence thesis by A11;

      end;

      hence thesis by A7, PARTFUN1: 5;

    end;

    theorem :: MESFUNC6:65

     0 <= r implies ( max+ (( - r) (#) f)) = (r (#) ( max- f)) & ( max- (( - r) (#) f)) = (r (#) ( max+ f))

    proof

      assume

       A1: 0 <= r;

      

       A2: ( dom ( max+ (( - r) (#) f))) = ( dom (( - r) (#) f)) by RFUNCT_3:def 10;

      then ( dom ( max+ (( - r) (#) f))) = ( dom f) by VALUED_1:def 5;

      then

       A3: ( dom ( max+ (( - r) (#) f))) = ( dom ( max- f)) by RFUNCT_3:def 11;

      then

       A4: ( dom ( max+ (( - r) (#) f))) = ( dom (r (#) ( max- f))) by VALUED_1:def 5;

      reconsider rr = r as Real;

      for x be Element of X st x in ( dom ( max+ (( - r) (#) f))) holds (( max+ (( - r) (#) f)) . x) = ((r (#) ( max- f)) . x)

      proof

        let x be Element of X;

        assume

         A5: x in ( dom ( max+ (( - r) (#) f)));

        

        then

         A6: (( max+ (( - r) (#) f)) . x) = ( max+ ((( - r) (#) f) . x)) by RFUNCT_3:def 10

        .= ( max ((( - r) * (f . x)), 0 )) by A2, A5, VALUED_1:def 5;

        ((r (#) ( max- f)) . x) = (r * (( max- f) . x)) by A4, A5, VALUED_1:def 5

        .= (rr * ( max- (f . x))) by A3, A5, RFUNCT_3:def 11

        .= ( max ((rr * ( - (f . x) qua Real) qua Real),(rr * 0 ))) by A1, FUZZY_2: 41;

        hence thesis by A6;

      end;

      hence ( max+ (( - r) (#) f)) = (r (#) ( max- f)) by A4, PARTFUN1: 5;

      

       A7: ( dom ( max- (( - r) (#) f))) = ( dom (( - r) (#) f)) by RFUNCT_3:def 11;

      then ( dom ( max- (( - r) (#) f))) = ( dom f) by VALUED_1:def 5;

      then

       A8: ( dom ( max- (( - r) (#) f))) = ( dom ( max+ f)) by RFUNCT_3:def 10;

      then

       A9: ( dom ( max- (( - r) (#) f))) = ( dom (r (#) ( max+ f))) by VALUED_1:def 5;

      for x be Element of X st x in ( dom ( max- (( - r) (#) f))) holds (( max- (( - r) (#) f)) . x) = ((r (#) ( max+ f)) . x)

      proof

        let x be Element of X;

        assume

         A10: x in ( dom ( max- (( - r) (#) f)));

        

        then

         A11: (( max- (( - r) (#) f)) . x) = ( max- ((( - r) (#) f) . x)) by RFUNCT_3:def 11

        .= ( max (( - (( - r) * (f . x))), 0 )) by A7, A10, VALUED_1:def 5;

        ((r (#) ( max+ f)) . x) = (r * (( max+ f) . x)) by A9, A10, VALUED_1:def 5

        .= (rr * ( max+ (f . x))) by A8, A10, RFUNCT_3:def 10

        .= ( max ((rr * (f . x)),(rr * 0 ))) by A1, FUZZY_2: 41;

        hence thesis by A11;

      end;

      hence thesis by A9, PARTFUN1: 5;

    end;

    theorem :: MESFUNC6:66

    ( max+ (f | Y)) = (( max+ f) | Y) & ( max- (f | Y)) = (( max- f) | Y)

    proof

      

       A1: ( dom ( max+ (f | Y))) = ( dom (f | Y)) by RFUNCT_3:def 10

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

      .= (( dom ( max+ f)) /\ Y) by RFUNCT_3:def 10

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

      for x be Element of X st x in ( dom ( max+ (f | Y))) holds (( max+ (f | Y)) . x) = ((( max+ f) | Y) . x)

      proof

        let x be Element of X;

        assume

         A2: x in ( dom ( max+ (f | Y)));

        then

         A3: x in (( dom ( max+ f)) /\ Y) by A1, RELAT_1: 61;

        then

         A4: x in Y by XBOOLE_0:def 4;

        

         A5: x in ( dom ( max+ f)) by A3, XBOOLE_0:def 4;

        

         A6: (( max+ (f | Y)) . x) = ( max+ ((f | Y) . x)) by A2, RFUNCT_3:def 10

        .= ( max ((f . x), 0 )) by A4, FUNCT_1: 49;

        ((( max+ f) | Y) . x) = (( max+ f) . x) by A1, A2, FUNCT_1: 47

        .= ( max+ (f . x)) by A5, RFUNCT_3:def 10;

        hence thesis by A6;

      end;

      hence ( max+ (f | Y)) = (( max+ f) | Y) by A1, PARTFUN1: 5;

      

       A7: ( dom ( max- (f | Y))) = ( dom (f | Y)) by RFUNCT_3:def 11

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

      .= (( dom ( max- f)) /\ Y) by RFUNCT_3:def 11

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

      for x be Element of X st x in ( dom ( max- (f | Y))) holds (( max- (f | Y)) . x) = ((( max- f) | Y) . x)

      proof

        let x be Element of X;

        assume

         A8: x in ( dom ( max- (f | Y)));

        then

         A9: x in (( dom ( max- f)) /\ Y) by A7, RELAT_1: 61;

        then

         A10: x in Y by XBOOLE_0:def 4;

        

         A11: x in ( dom ( max- f)) by A9, XBOOLE_0:def 4;

        

         A12: (( max- (f | Y)) . x) = ( max- ((f | Y) . x)) by A8, RFUNCT_3:def 11

        .= ( max (( - (f . x)), 0 )) by A10, FUNCT_1: 49;

        ((( max- f) | Y) . x) = (( max- f) . x) by A7, A8, FUNCT_1: 47

        .= ( max- (f . x)) by A11, RFUNCT_3:def 11;

        hence thesis by A12;

      end;

      hence thesis by A7, PARTFUN1: 5;

    end;

    theorem :: MESFUNC6:67

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

    proof

      assume

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

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

      .= ((( dom f) /\ Y) /\ (( dom g) /\ Y)) by RELAT_1: 61

      .= (((( dom f) /\ Y) /\ ( dom g)) /\ Y) by XBOOLE_1: 16

      .= (((( dom f) /\ ( dom g)) /\ Y) /\ Y) by XBOOLE_1: 16

      .= ((( dom f) /\ ( dom g)) /\ (Y /\ Y)) by XBOOLE_1: 16;

      

      then

       A2: ( dom ((f | Y) + (g | Y))) = ((( dom f) /\ ( dom g)) /\ Y) by VALUED_1:def 1

      .= (( dom (f + g)) /\ Y) by VALUED_1:def 1

      .= Y by A1, XBOOLE_1: 28;

      

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

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

      then

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

      

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

      then

       A6: ( dom ((f + g) | Y)) = Y by A1, XBOOLE_1: 28;

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

      then

       A7: ( dom (f | Y)) = Y by A1, A3, XBOOLE_1: 18, XBOOLE_1: 28;

      now

        let x be object;

        assume

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

        

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

        .= ((f . x) + (g . x)) by A1, A6, A8, VALUED_1:def 1

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

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

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

      end;

      hence thesis by A1, A5, A2, FUNCT_1: 2, XBOOLE_1: 28;

    end;

    theorem :: MESFUNC6:68

    ( eq_dom (f,r)) = (f " {r})

    proof

      now

        let x be object;

        assume

         A1: x in (f " {r});

        then (f . x) in {r} by FUNCT_1:def 7;

        then

         A2: (( R_EAL f) . x) = r by TARSKI:def 1;

        x in ( dom f) by A1, FUNCT_1:def 7;

        hence x in ( eq_dom (f,r)) by A2, MESFUNC1:def 15;

      end;

      then

       A3: (f " {r}) c= ( eq_dom (f,r));

      now

        let x be object;

        assume

         A4: x in ( eq_dom (f,r));

        then r = (f . x) by MESFUNC1:def 15;

        then

         A5: (f . x) in {r} by TARSKI:def 1;

        x in ( dom f) by A4, MESFUNC1:def 15;

        hence x in (f " {r}) by A5, FUNCT_1:def 7;

      end;

      then ( eq_dom (f,r)) c= (f " {r});

      hence thesis by A3;

    end;

    begin

    reserve X for non empty set,

S for SigmaField of X,

f,g for PartFunc of X, REAL ,

A,B for Element of S,

r,s for Real;

    theorem :: MESFUNC6:69

    f is A -measurable & A c= ( dom f) implies ((A /\ ( great_eq_dom (f,r))) /\ ( less_dom (f,s))) in S

    proof

      assume that

       A1: f is A -measurable and

       A2: A c= ( dom f);

      ( R_EAL f) is A -measurable by A1;

      then

       A3: (A /\ ( less_dom (( R_EAL f),s))) in S by MESFUNC1:def 16;

      

       A4: ((A /\ ( great_eq_dom (f,r))) /\ (A /\ ( less_dom (f,s)))) = (((A /\ ( great_eq_dom (f,r))) /\ A) /\ ( less_dom (f,s))) by XBOOLE_1: 16

      .= ((( great_eq_dom (f,r)) /\ (A /\ A)) /\ ( less_dom (f,s))) by XBOOLE_1: 16;

      (A /\ ( great_eq_dom (f,r))) in S by A1, A2, Th13;

      hence thesis by A3, A4, FINSUB_1:def 2;

    end;

    theorem :: MESFUNC6:70

    

     Th70: f is_simple_func_in S implies (f | A) is_simple_func_in S

    proof

      assume f is_simple_func_in S;

      then

      consider F be Finite_Sep_Sequence of S such that

       A1: ( dom f) = ( union ( rng F)) and

       A2: for n be Nat, x,y be Element of X st n in ( dom F) & x in (F . n) & y in (F . n) holds (f . x) = (f . y);

      deffunc FA( Nat) = ((F . $1) /\ A);

      consider G be FinSequence such that

       A3: ( len G) = ( len F) & for n be Nat st n in ( dom G) holds (G . n) = FA(n) from FINSEQ_1:sch 2;

      

       A4: ( rng G) c= S

      proof

        let P be object;

        assume P in ( rng G);

        then

        consider k be object such that

         A5: k in ( dom G) and

         A6: P = (G . k) by FUNCT_1:def 3;

        reconsider k as Element of NAT by A5;

        k in ( Seg ( len F)) by A3, A5, FINSEQ_1:def 3;

        then k in ( dom F) by FINSEQ_1:def 3;

        then

         A7: (F . k) in ( rng F) by FUNCT_1: 3;

        (G . k) = ((F . k) /\ A) by A3, A5;

        hence thesis by A6, A7, FINSUB_1:def 2;

      end;

      

       A8: ( dom G) = ( Seg ( len F)) by A3, FINSEQ_1:def 3;

      reconsider G as FinSequence of S by A4, FINSEQ_1:def 4;

      for i,j be Nat st i in ( dom G) & j in ( dom G) & i <> j holds (G . i) misses (G . j)

      proof

        let i,j be Nat;

        assume that

         A9: i in ( dom G) and

         A10: j in ( dom G) and

         A11: i <> j;

        j in ( Seg ( len F)) by A3, A10, FINSEQ_1:def 3;

        then

         A12: j in ( dom F) by FINSEQ_1:def 3;

        i in ( Seg ( len F)) by A3, A9, FINSEQ_1:def 3;

        then i in ( dom F) by FINSEQ_1:def 3;

        then

         A13: (F . i) misses (F . j) by A11, A12, MESFUNC3: 4;

        (G . i) = ((F . i) /\ A) & (G . j) = ((F . j) /\ A) by A3, A9, A10;

        

        then ((G . i) /\ (G . j)) = ((((F . i) /\ A) /\ (F . j)) /\ A) by XBOOLE_1: 16

        .= ((((F . i) /\ (F . j)) /\ A) /\ A) by XBOOLE_1: 16

        .= (( {} /\ A) /\ A) by A13;

        hence thesis;

      end;

      then

      reconsider G as Finite_Sep_Sequence of S by MESFUNC3: 4;

      for v be object st v in ( union ( rng G)) holds v in ( dom (f | A))

      proof

        let v be object;

        assume v in ( union ( rng G));

        then

        consider W be set such that

         A14: v in W and

         A15: W in ( rng G) by TARSKI:def 4;

        consider k be object such that

         A16: k in ( dom G) and

         A17: W = (G . k) by A15, FUNCT_1:def 3;

        reconsider k as Element of NAT by A16;

        k in ( Seg ( len F)) by A3, A16, FINSEQ_1:def 3;

        then k in ( dom F) by FINSEQ_1:def 3;

        then

         A18: (F . k) in ( rng F) by FUNCT_1: 3;

        

         A19: (G . k) = ((F . k) /\ A) by A3, A16;

        then v in (F . k) by A14, A17, XBOOLE_0:def 4;

        then

         A20: v in ( union ( rng F)) by A18, TARSKI:def 4;

        v in A by A14, A17, A19, XBOOLE_0:def 4;

        then v in (( dom f) /\ A) by A1, A20, XBOOLE_0:def 4;

        hence thesis by RELAT_1: 61;

      end;

      then

       A21: ( union ( rng G)) c= ( dom (f | A));

      for v be object st v in ( dom (f | A)) holds v in ( union ( rng G))

      proof

        let v be object;

        assume v in ( dom (f | A));

        then

         A22: v in (( dom f) /\ A) by RELAT_1: 61;

        then

         A23: v in A by XBOOLE_0:def 4;

        v in ( dom f) by A22, XBOOLE_0:def 4;

        then

        consider W be set such that

         A24: v in W and

         A25: W in ( rng F) by A1, TARSKI:def 4;

        consider k be object such that

         A26: k in ( dom F) and

         A27: W = (F . k) by A25, FUNCT_1:def 3;

        reconsider k as Element of NAT by A26;

        

         A28: k in ( Seg ( len F)) by A26, FINSEQ_1:def 3;

        then k in ( dom G) by A3, FINSEQ_1:def 3;

        then

         A29: (G . k) in ( rng G) by FUNCT_1: 3;

        (G . k) = ((F . k) /\ A) by A3, A8, A28;

        then v in (G . k) by A23, A24, A27, XBOOLE_0:def 4;

        hence thesis by A29, TARSKI:def 4;

      end;

      then ( dom (f | A)) c= ( union ( rng G));

      then

       A30: ( dom (f | A)) = ( union ( rng G)) by A21;

      for n be Nat, x,y be Element of X st n in ( dom G) & x in (G . n) & y in (G . n) holds ((f | A) . x) = ((f | A) . y)

      proof

        let n be Nat;

        let x,y be Element of X;

        assume that

         A31: n in ( dom G) and

         A32: x in (G . n) and

         A33: y in (G . n);

        n in ( Seg ( len F)) by A3, A31, FINSEQ_1:def 3;

        then

         A34: n in ( dom F) by FINSEQ_1:def 3;

        (G . n) = ((F . n) /\ A) by A3, A31;

        then x in (F . n) & y in (F . n) by A32, A33, XBOOLE_0:def 4;

        then

         A35: (f . x) = (f . y) by A2, A34;

        

         A36: (G . n) in ( rng G) by A31, FUNCT_1: 3;

        then x in ( dom (f | A)) by A30, A32, TARSKI:def 4;

        then

         A37: ((f | A) . x) = (f . y) by A35, FUNCT_1: 47;

        y in ( dom (f | A)) by A30, A33, A36, TARSKI:def 4;

        hence thesis by A37, FUNCT_1: 47;

      end;

      hence thesis by A30;

    end;

    theorem :: MESFUNC6:71

    

     Th71: f is_simple_func_in S implies ( dom f) is Element of S by MESFUNC2: 31;

    

     Lm1: 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_simple_func_in S & ( dom f) <> {} & g is_simple_func_in S & ( dom g) = ( dom f) holds (f + g) is_simple_func_in S & ( dom (f + g)) <> {}

    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 such that

       A1: f is_simple_func_in S and

       A2: ( dom f) <> {} and

       A3: g is_simple_func_in S and

       A4: ( dom g) = ( dom f);

      ( R_EAL f) is_simple_func_in S by A1, Th49;

      then

      consider F be Finite_Sep_Sequence of S, a be FinSequence of ExtREAL such that

       A5: (F,a) are_Re-presentation_of ( R_EAL f) by MESFUNC3: 12;

      set la = ( len F);

      

       A6: ( dom f) = ( union ( rng F)) by A5, MESFUNC3:def 1;

      ( R_EAL g) is_simple_func_in S by A3, Th49;

      then

      consider G be Finite_Sep_Sequence of S, b be FinSequence of ExtREAL such that

       A7: (G,b) are_Re-presentation_of ( R_EAL g) by MESFUNC3: 12;

      set lb = ( len G);

      

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

      deffunc FG1( Nat) = ((F . ((($1 -' 1) div lb) + 1)) /\ (G . ((($1 -' 1) mod lb) + 1)));

      consider FG be FinSequence such that

       A9: ( len FG) = (la * lb) and

       A10: for k be Nat st k in ( dom FG) holds (FG . k) = FG1(k) from FINSEQ_1:sch 2;

      

       A11: ( dom FG) = ( Seg (la * lb)) by A9, FINSEQ_1:def 3;

      now

        reconsider la9 = la, lb9 = lb as Nat;

        let k be Nat;

        set i = (((k -' 1) div lb) + 1);

        set j = (((k -' 1) mod lb) + 1);

        assume

         A12: k in ( dom FG);

        then

         A13: k in ( Seg (la * lb)) by A9, FINSEQ_1:def 3;

        then

         A14: k <= (la * lb) by FINSEQ_1: 1;

        then (k -' 1) <= ((la * lb) -' 1) by NAT_D: 42;

        then

         A15: ((k -' 1) div lb) <= (((la * lb) -' 1) div lb) by NAT_2: 24;

        1 <= k by A13, FINSEQ_1: 1;

        then

         A16: lb9 divides (la9 * lb9) & 1 <= (la * lb) by A14, NAT_D:def 3, XXREAL_0: 2;

        

         A17: lb <> 0 by A13, A14, FINSEQ_1: 1;

        then lb >= ( 0 + 1) by NAT_1: 13;

        then (((la9 * lb9) -' 1) div lb9) = (((la9 * lb9) div lb9) - 1) by A16, NAT_2: 15;

        then (((k -' 1) div lb) + 1) <= ((la * lb) div lb) by A15, XREAL_1: 19;

        then i >= ( 0 + 1) & i <= la by A17, NAT_D: 18, XREAL_1: 6;

        then i in ( Seg la);

        then i in ( dom F) by FINSEQ_1:def 3;

        then

         A18: (F . i) in ( rng F) by FUNCT_1: 3;

        ((k -' 1) mod lb) < lb by A17, NAT_D: 1;

        then j >= ( 0 + 1) & j <= lb by NAT_1: 13;

        then j in ( dom G) by FINSEQ_3: 25;

        then (G . j) in ( rng G) by FUNCT_1: 3;

        then ((F . i) /\ (G . j)) in S by A18, MEASURE1: 34;

        hence (FG . k) in S by A10, A12;

      end;

      then

      reconsider FG as FinSequence of S by FINSEQ_2: 12;

      for k,l be Nat st k in ( dom FG) & l in ( dom FG) & k <> l holds (FG . k) misses (FG . l)

      proof

        reconsider la9 = la, lb9 = lb as Nat;

        let k,l be Nat;

        assume that

         A19: k in ( dom FG) and

         A20: l in ( dom FG) and

         A21: k <> l;

        set j = (((k -' 1) mod lb) + 1);

        set i = (((k -' 1) div lb) + 1);

        

         A22: (FG . k) = ((F . i) /\ (G . j)) by A10, A19;

        set m = (((l -' 1) mod lb) + 1);

        set n = (((l -' 1) div lb) + 1);

        

         A23: k in ( Seg (la * lb)) by A9, A19, FINSEQ_1:def 3;

        then

         A24: 1 <= k by FINSEQ_1: 1;

        then

         A25: lb <> 0 by A23, FINSEQ_1: 1;

        then ((k -' 1) mod lb) < lb by NAT_D: 1;

        then j >= ( 0 + 1) & j <= lb by NAT_1: 13;

        then

         A26: j in ( dom G) by FINSEQ_3: 25;

        

         A27: k <= (la * lb) by A23, FINSEQ_1: 1;

        then

         A28: lb9 divides (la9 * lb9) & 1 <= (la * lb) by A24, NAT_D:def 3, XXREAL_0: 2;

        lb >= ( 0 + 1) by A25, NAT_1: 13;

        then

         A29: (((la9 * lb9) -' 1) div lb9) = (((la9 * lb9) div lb9) - 1) by A28, NAT_2: 15;

        

         A30: l in ( Seg (la * lb)) by A9, A20, FINSEQ_1:def 3;

        then

         A31: 1 <= l by FINSEQ_1: 1;

         A32:

        now

          ((l -' 1) + 1) = ((((n - 1) * lb) + (m - 1)) + 1) by A25, NAT_D: 2;

          then

           A33: ((l - 1) + 1) = (((n - 1) * lb) + m) by A31, XREAL_1: 233;

          ((k -' 1) + 1) = ((((i - 1) * lb) + (j - 1)) + 1) by A25, NAT_D: 2;

          then

           A34: ((k - 1) + 1) = (((i - 1) * lb) + j) by A24, XREAL_1: 233;

          assume i = n & j = m;

          hence contradiction by A21, A34, A33;

        end;

        (k -' 1) <= ((la * lb) -' 1) by A27, NAT_D: 42;

        then ((k -' 1) div lb) <= (((la * lb) div lb) - 1) by A29, NAT_2: 24;

        then (((k -' 1) div lb) + 1) <= ((la * lb) div lb) by XREAL_1: 19;

        then i >= ( 0 + 1) & i <= la by A25, NAT_D: 18, XREAL_1: 6;

        then i in ( Seg la);

        then

         A35: i in ( dom F) by FINSEQ_1:def 3;

        ((l -' 1) mod lb) < lb by A25, NAT_D: 1;

        then m >= ( 0 + 1) & m <= lb by NAT_1: 13;

        then

         A36: m in ( dom G) by FINSEQ_3: 25;

        l <= (la * lb) by A30, FINSEQ_1: 1;

        then (l -' 1) <= ((la * lb) -' 1) by NAT_D: 42;

        then ((l -' 1) div lb) <= (((la * lb) div lb) - 1) by A29, NAT_2: 24;

        then (((l -' 1) div lb) + 1) <= ((la * lb) div lb) by XREAL_1: 19;

        then n >= ( 0 + 1) & n <= la by A25, NAT_D: 18, XREAL_1: 6;

        then n in ( Seg la);

        then

         A37: n in ( dom F) by FINSEQ_1:def 3;

        per cases by A32;

          suppose

           A38: i <> n;

          ((FG . k) /\ (FG . l)) = (((F . i) /\ (G . j)) /\ ((F . n) /\ (G . m))) by A10, A20, A22;

          then ((FG . k) /\ (FG . l)) = ((F . i) /\ ((G . j) /\ ((F . n) /\ (G . m)))) by XBOOLE_1: 16;

          then ((FG . k) /\ (FG . l)) = ((F . i) /\ ((F . n) /\ ((G . j) /\ (G . m)))) by XBOOLE_1: 16;

          then

           A39: ((FG . k) /\ (FG . l)) = (((F . i) /\ (F . n)) /\ ((G . j) /\ (G . m))) by XBOOLE_1: 16;

          (F . i) misses (F . n) by A35, A37, A38, MESFUNC3: 4;

          then ((FG . k) /\ (FG . l)) = ( {} /\ ((G . j) /\ (G . m))) by A39;

          hence thesis;

        end;

          suppose

           A40: j <> m;

          ((FG . k) /\ (FG . l)) = (((F . i) /\ (G . j)) /\ ((F . n) /\ (G . m))) by A10, A20, A22;

          then ((FG . k) /\ (FG . l)) = ((F . i) /\ ((G . j) /\ ((F . n) /\ (G . m)))) by XBOOLE_1: 16;

          then ((FG . k) /\ (FG . l)) = ((F . i) /\ ((F . n) /\ ((G . j) /\ (G . m)))) by XBOOLE_1: 16;

          then

           A41: ((FG . k) /\ (FG . l)) = (((F . i) /\ (F . n)) /\ ((G . j) /\ (G . m))) by XBOOLE_1: 16;

          (G . j) misses (G . m) by A26, A36, A40, MESFUNC3: 4;

          then ((FG . k) /\ (FG . l)) = (((F . i) /\ (F . n)) /\ {} ) by A41;

          hence thesis;

        end;

      end;

      then

      reconsider FG as Finite_Sep_Sequence of S by MESFUNC3: 4;

      

       A42: ( dom g) = ( union ( rng G)) by A7, MESFUNC3:def 1;

      

       A43: ( dom f) = ( union ( rng FG))

      proof

        now

          let z be object;

          assume

           A44: z in ( dom f);

          then

          consider Y be set such that

           A45: z in Y and

           A46: Y in ( rng F) by A6, TARSKI:def 4;

          consider i be Nat such that

           A47: i in ( dom F) and

           A48: Y = (F . i) by A46, FINSEQ_2: 10;

          

           A49: i in ( Seg ( len F)) by A47, FINSEQ_1:def 3;

          then 1 <= i by FINSEQ_1: 1;

          then

          consider i9 be Nat such that

           A50: i = (1 + i9 qua Complex) by NAT_1: 10;

          consider Z be set such that

           A51: z in Z and

           A52: Z in ( rng G) by A4, A42, A44, TARSKI:def 4;

          consider j be Nat such that

           A53: j in ( dom G) and

           A54: Z = (G . j) by A52, FINSEQ_2: 10;

          

           A55: j in ( Seg ( len G)) by A53, FINSEQ_1:def 3;

          then

           A56: 1 <= j by FINSEQ_1: 1;

          then

          consider j9 be Nat such that

           A57: j = (1 + j9 qua Complex) by NAT_1: 10;

          

           A58: j <= lb by A55, FINSEQ_1: 1;

          then

           A59: j9 < lb by A57, NAT_1: 13;

          reconsider k = (((i - 1) * lb) + j) as Nat by A50;

          

           A60: k >= ( 0 + j) by A50, XREAL_1: 6;

          

          then

           A61: (k -' 1) = (k - 1) by A56, XREAL_1: 233, XXREAL_0: 2

          .= ((i9 * lb) + j9) by A50, A57;

          then

           A62: i = (((k -' 1) div lb) + 1) by A50, A59, NAT_D:def 1;

          i <= la by A49, FINSEQ_1: 1;

          then (i - 1) <= (la - 1) by XREAL_1: 9;

          then ((i - 1) * lb) <= ((la - 1) * lb) by XREAL_1: 64;

          then

           A63: k <= (((la - 1) * lb) + j) by XREAL_1: 6;

          (((la - 1) * lb) + j) <= (((la - 1) * lb) + lb) by A58, XREAL_1: 6;

          then

           A64: k <= (la * lb) by A63, XXREAL_0: 2;

          k >= 1 by A56, A60, XXREAL_0: 2;

          then

           A65: k in ( Seg (la * lb)) by A64;

          then k in ( dom FG) by A9, FINSEQ_1:def 3;

          then

           A66: (FG . k) in ( rng FG) by FUNCT_1:def 3;

          

           A67: j = (((k -' 1) mod lb) + 1) by A57, A61, A59, NAT_D:def 2;

          z in ((F . i) /\ (G . j)) by A45, A48, A51, A54, XBOOLE_0:def 4;

          then z in (FG . k) by A10, A11, A62, A67, A65;

          hence z in ( union ( rng FG)) by A66, TARSKI:def 4;

        end;

        hence ( dom f) c= ( union ( rng FG));

        reconsider la9 = la, lb9 = lb as Nat;

        let z be object;

        assume z in ( union ( rng FG));

        then

        consider Y be set such that

         A68: z in Y and

         A69: Y in ( rng FG) by TARSKI:def 4;

        consider k be Nat such that

         A70: k in ( dom FG) and

         A71: Y = (FG . k) by A69, FINSEQ_2: 10;

        set j = (((k -' 1) mod lb) + 1);

        set i = (((k -' 1) div lb) + 1);

        

         A72: k in ( Seg ( len FG)) by A70, FINSEQ_1:def 3;

        then

         A73: k <= (la * lb) by A9, FINSEQ_1: 1;

        then

         A74: lb <> 0 by A72, FINSEQ_1: 1;

        then

         A75: lb >= ( 0 + 1) by NAT_1: 13;

        1 <= k by A72, FINSEQ_1: 1;

        then lb9 divides (la9 * lb9) & 1 <= (la * lb) by A73, NAT_D:def 3, XXREAL_0: 2;

        then

         A76: (((la9 * lb9) -' 1) div lb9) = (((la9 * lb9) div lb9) - 1) by A75, NAT_2: 15;

        (k -' 1) <= ((la * lb) -' 1) by A73, NAT_D: 42;

        then ((k -' 1) div lb) <= (((la * lb) div lb) - 1) by A76, NAT_2: 24;

        then

         A77: i <= ((la * lb) div lb) by XREAL_1: 19;

        i >= ( 0 + 1) & ((la * lb) div lb) = la by A74, NAT_D: 18, XREAL_1: 6;

        then i in ( Seg la) by A77;

        then i in ( dom F) by FINSEQ_1:def 3;

        then

         A78: (F . i) in ( rng F) by FUNCT_1:def 3;

        (FG . k) = ((F . i) /\ (G . j)) by A10, A70;

        then z in (F . i) by A68, A71, XBOOLE_0:def 4;

        hence thesis by A6, A78, TARSKI:def 4;

      end;

      for k be Nat, x,y be Element of X st k in ( dom FG) & x in (FG . k) & y in (FG . k) holds ((f + g) . x) = ((f + g) . y)

      proof

        reconsider la9 = la, lb9 = lb as Nat;

        let k be Nat;

        let x,y be Element of X;

        assume that

         A79: k in ( dom FG) and

         A80: x in (FG . k) and

         A81: y in (FG . k);

        set i = (((k -' 1) div lb) + 1);

        set j = (((k -' 1) mod lb) + 1);

        

         A82: k in ( Seg ( len FG)) by A79, FINSEQ_1:def 3;

        then

         A83: k <= (la * lb) by A9, FINSEQ_1: 1;

        then

         A84: (k -' 1) <= ((la * lb) -' 1) by NAT_D: 42;

        

         A85: lb <> 0 by A82, A83, FINSEQ_1: 1;

        then ((k -' 1) mod lb) < lb by NAT_D: 1;

        then j >= ( 0 + 1) & j <= lb by NAT_1: 13;

        then j in ( Seg lb);

        then

         A86: j in ( dom G) by FINSEQ_1:def 3;

        1 <= k by A82, FINSEQ_1: 1;

        then

         A87: lb9 divides (la9 * lb9) & 1 <= (la * lb) by A83, NAT_D:def 3, XXREAL_0: 2;

        lb >= ( 0 + 1) by A85, NAT_1: 13;

        then (((la9 * lb9) -' 1) div lb9) = (((la9 * lb9) div lb9) - 1) by A87, NAT_2: 15;

        then ((k -' 1) div lb) <= (((la * lb) div lb) - 1) by A84, NAT_2: 24;

        then (((k -' 1) div lb) + 1) <= ((la * lb) div lb) by XREAL_1: 19;

        then i >= ( 0 + 1) & i <= la by A85, NAT_D: 18, XREAL_1: 6;

        then i in ( Seg la);

        then

         A88: i in ( dom F) by FINSEQ_1:def 3;

        

         A89: (FG . k) = ((F . (((k -' 1) div lb) + 1)) /\ (G . (((k -' 1) mod lb) + 1))) by A10, A79;

        then x in (G . j) by A80, XBOOLE_0:def 4;

        then

         A90: (g . x) = (b . j) by A7, A86, MESFUNC3:def 1;

        y in (G . j) by A81, A89, XBOOLE_0:def 4;

        then

         A91: (g . y) = (b . j) by A7, A86, MESFUNC3:def 1;

        x in (F . i) by A80, A89, XBOOLE_0:def 4;

        then (f . x) = (a . i) by A5, A88, MESFUNC3:def 1;

        then

         A92: ((f . x) + (g . x)) = ((a . i) + (b . j)) by A90;

        y in (F . i) by A81, A89, XBOOLE_0:def 4;

        then

         A93: (f . y) = (a . i) by A5, A88, MESFUNC3:def 1;

        

         A94: (FG . k) in ( rng FG) by A79, FUNCT_1:def 3;

        then x in ( dom (f + g)) by A4, A43, A8, A80, TARSKI:def 4;

        then ((f + g) . x) = ((a . i) + (b . j)) by A92, VALUED_1:def 1;

        then

         A95: ((f + g) . x) = ((f . y) + (g . y)) by A93, A91;

        y in ( dom (f + g)) by A4, A43, A8, A81, A94, TARSKI:def 4;

        hence thesis by A95, VALUED_1:def 1;

      end;

      hence (f + g) is_simple_func_in S by A4, A43, A8;

      thus thesis by A2, A4, A8;

    end;

    theorem :: MESFUNC6:72

    f is_simple_func_in S & g is_simple_func_in S implies (f + g) is_simple_func_in S

    proof

      assume

       A1: f is_simple_func_in S & g is_simple_func_in S;

      per cases ;

        suppose

         A2: ( dom (f + g)) = {} ;

        ex F be Finite_Sep_Sequence of S st (( dom (f + g)) = ( union ( rng F)) & for n be Nat, x,y be Element of X st n in ( dom F) & x in (F . n) & y in (F . n) holds ((f + g) . x) = ((f + g) . y))

        proof

          reconsider EMPTY = {} as Element of S by PROB_1: 4;

          set F = <*EMPTY*>;

          

           A3: ( dom F) = ( Seg 1) by FINSEQ_1: 38;

           A4:

          now

            let i,j be Nat;

            assume that

             A5: i in ( dom F) and

             A6: j in ( dom F) & i <> j;

            i = 1 by A3, A5, FINSEQ_1: 2, TARSKI:def 1;

            hence (F . i) misses (F . j) by A3, A6, FINSEQ_1: 2, TARSKI:def 1;

          end;

          

           A7: for n be Nat st n in ( dom F) holds (F . n) = EMPTY

          proof

            let n be Nat;

            assume n in ( dom F);

            then n = 1 by A3, FINSEQ_1: 2, TARSKI:def 1;

            hence thesis by FINSEQ_1: 40;

          end;

          reconsider F as Finite_Sep_Sequence of S by A4, MESFUNC3: 4;

          take F;

          ( union ( rng F)) = ( union ( bool {} )) by FINSEQ_1: 39, ZFMISC_1: 1;

          hence ( dom (f + g)) = ( union ( rng F)) by A2;

          thus thesis by A7;

        end;

        hence thesis;

      end;

        suppose

         A8: ( dom (f + g)) <> {} ;

        

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

        ( dom f) is Element of S & ( dom g) is Element of S by A1, Th71;

        then ( dom (f + g)) in S by A9, FINSUB_1:def 2;

        then

         A10: (f | ( dom (f + g))) is_simple_func_in S & (g | ( dom (f + g))) is_simple_func_in S by A1, Th70;

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

        then

         A11: ( dom (f | ( dom (f + g)))) = ((( dom f) /\ ( dom f)) /\ ( dom g)) by A9, XBOOLE_1: 16;

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

        then

         A12: ( dom (g | ( dom (f + g)))) = ((( dom g) /\ ( dom g)) /\ ( dom f)) by A9, XBOOLE_1: 16;

        then

         A13: ( dom (g | ( dom (f + g)))) = ( dom (f + g)) by VALUED_1:def 1;

        

         A14: ( dom ((f | ( dom (f + g))) + (g | ( dom (f + g))))) = (( dom (f | ( dom (f + g)))) /\ ( dom (g | ( dom (f + g))))) by VALUED_1:def 1

        .= ( dom (f + g)) by A11, A12, VALUED_1:def 1;

        

         A15: for x be Element of X st x in ( dom ((f | ( dom (f + g))) + (g | ( dom (f + g))))) holds (((f | ( dom (f + g))) + (g | ( dom (f + g)))) . x) = ((f + g) . x)

        proof

          let x be Element of X;

          assume

           A16: x in ( dom ((f | ( dom (f + g))) + (g | ( dom (f + g)))));

          

          then (((f | ( dom (f + g))) + (g | ( dom (f + g)))) . x) = (((f | ( dom (f + g))) . x) + ((g | ( dom (f + g))) . x)) by VALUED_1:def 1

          .= ((f . x) + ((g | ( dom (f + g))) . x)) by A14, A16, FUNCT_1: 49

          .= ((f . x) + (g . x)) by A14, A16, FUNCT_1: 49;

          hence thesis by A14, A16, VALUED_1:def 1;

        end;

        ( dom (f | ( dom (f + g)))) = ( dom (f + g)) by A11, VALUED_1:def 1;

        then ((f | ( dom (f + g))) + (g | ( dom (f + g)))) is_simple_func_in S by A8, A10, A13, Lm1;

        hence thesis by A14, A15, PARTFUN1: 5;

      end;

    end;

    theorem :: MESFUNC6:73

    f is_simple_func_in S implies (r (#) f) is_simple_func_in S

    proof

      set g = (r (#) f);

      assume f is_simple_func_in S;

      then

      consider G be Finite_Sep_Sequence of S such that

       A1: ( dom f) = ( union ( rng G)) and

       A2: for n be Nat, x,y be Element of X st n in ( dom G) & x in (G . n) & y in (G . n) holds (f . x) = (f . y);

      

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

      now

        let n be Nat;

        let x,y be Element of X;

        assume that

         A4: n in ( dom G) and

         A5: x in (G . n) and

         A6: y in (G . n);

        

         A7: (G . n) in ( rng G) by A4, FUNCT_1: 3;

        then y in ( dom g) by A3, A1, A6, TARSKI:def 4;

        then

         A8: (g . y) = (r * (f . y)) by VALUED_1:def 5;

        x in ( dom g) by A3, A1, A5, A7, TARSKI:def 4;

        then (g . x) = (r * (f . x)) by VALUED_1:def 5;

        hence (g . x) = (g . y) by A2, A4, A5, A6, A8;

      end;

      hence thesis by A3, A1;

    end;

    theorem :: MESFUNC6:74

    (for x be set st x in ( dom (f - g)) holds (g . x) <= (f . x)) implies (f - g) is nonnegative

    proof

      

       A1: ( dom (f - g)) = (( dom f) /\ ( dom g)) by VALUED_1: 12;

      assume for x be set st x in ( dom (f - g)) holds (g . x) <= (f . x);

      hence thesis by A1, Th58;

    end;

    theorem :: MESFUNC6:75

    ex f be PartFunc of X, REAL st f is_simple_func_in S & ( dom f) = A & for x be object st x in A holds (f . x) = r

    proof

      defpred P[ object] means $1 in A;

      deffunc F( object) = r;

      

       A1: for x be object st P[x] holds F(x) in REAL by XREAL_0:def 1;

      consider f be PartFunc of X, REAL such that

       A2: (for x be object holds x in ( dom f) iff x in X & P[x]) & for x be object st x in ( dom f) holds (f . x) = F(x) from PARTFUN1:sch 3( A1);

      take f;

      

       A3: A c= ( dom f) by A2;

      

       A4: ( dom f) c= A by A2;

      ex F be Finite_Sep_Sequence of S st (( dom f) = ( union ( rng F)) & for n be Nat, x,y be Element of X st n in ( dom F) & x in (F . n) & y in (F . n) holds (f . x) = (f . y))

      proof

        set F = <*( dom f)*>;

        

         A5: ( rng F) = {( dom f)} by FINSEQ_1: 38;

        then ( rng F) = {A} by A4, A3, XBOOLE_0:def 10;

        then

        reconsider F as FinSequence of S by FINSEQ_1:def 4;

        now

          let i,j be Nat such that

           A6: i in ( dom F) and

           A7: j in ( dom F) & i <> j;

          

           A8: ( dom F) = ( Seg 1) by FINSEQ_1: 38;

          then i = 1 by A6, FINSEQ_1: 2, TARSKI:def 1;

          hence (F . i) misses (F . j) by A7, A8, FINSEQ_1: 2, TARSKI:def 1;

        end;

        then

        reconsider F as Finite_Sep_Sequence of S by MESFUNC3: 4;

        take F;

        thus ( dom f) = ( union ( rng F)) by A5, ZFMISC_1: 25;

        hereby

          let n be Nat;

          let x,y be Element of X;

          assume that

           A9: n in ( dom F) and

           A10: x in (F . n) and

           A11: y in (F . n);

          ( dom F) = ( Seg 1) by FINSEQ_1: 38;

          then

           A12: n = 1 by A9, FINSEQ_1: 2, TARSKI:def 1;

          then x in ( dom f) by A10, FINSEQ_1: 40;

          then

           A13: (f . x) = r by A2;

          y in ( dom f) by A11, A12, FINSEQ_1: 40;

          hence (f . x) = (f . y) by A2, A13;

        end;

      end;

      hence f is_simple_func_in S;

      thus ( dom f) = A by A4, A3;

      thus thesis by A2;

    end;

    theorem :: MESFUNC6:76

    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: ( R_EAL f) is B -measurable by A1;

      now

        let r be Real;

        now

          let x be object;

          x in ( dom (f | B)) & ((f | B) . x) < r iff x in (( dom f) /\ B) & ((f | B) . x) < r by RELAT_1: 61;

          then

           A4: x in A & x in ( less_dom ((f | B),r)) iff x in B & x in ( dom f) & ((f | B) . x) < r by A2, MESFUNC1:def 11, XBOOLE_0:def 4;

          x in B & x in ( dom f) implies ((f . x) < r iff ((f | B) . x) < r) by FUNCT_1: 49;

          then x in (A /\ ( less_dom ((f | B),r))) iff x in B & x in ( less_dom (f,r)) by A4, MESFUNC1:def 11, XBOOLE_0:def 4;

          hence x in (A /\ ( less_dom ((f | B),r))) iff x in (B /\ ( less_dom (f,r))) by XBOOLE_0:def 4;

        end;

        then (A /\ ( less_dom ((f | B),r))) c= (B /\ ( less_dom (f,r))) & (B /\ ( less_dom (f,r))) c= (A /\ ( less_dom ((f | B),r)));

        then (A /\ ( less_dom ((f | B),r))) = (B /\ ( less_dom (f,r)));

        then (A /\ ( less_dom ((f | B),r))) in S by A3, MESFUNC1:def 16;

        hence (A /\ ( less_dom ((f | B),r))) in S;

      end;

      hence thesis by Th12;

    end;

    theorem :: MESFUNC6:77

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

    proof

      assume that

       A1: A c= ( dom f) and

       A2: f is A -measurable and

       A3: g is A -measurable;

      (f + g) is A -measurable by A2, A3, Th26;

      then

       A4: ( max+ (f + g)) is A -measurable by Th46;

      ( max- f) is A -measurable by A1, A2, Th47;

      hence thesis by A4, Th26;

    end;

    theorem :: MESFUNC6:78

    A c= (( dom f) /\ ( dom g)) & f is A -measurable & g is A -measurable implies (( max- (f + g)) + ( max+ f)) is A -measurable

    proof

      assume that

       A1: A c= (( dom f) /\ ( dom g)) and

       A2: f is A -measurable and

       A3: g is A -measurable;

      

       A4: ( max+ f) is A -measurable by A2, Th46;

      

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

      (f + g) is A -measurable by A2, A3, Th26;

      then ( max- (f + g)) is A -measurable by A1, A5, Th47;

      hence thesis by A4, Th26;

    end;

    theorem :: MESFUNC6:79

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

    proof

      assume ( dom f) in S & ( dom g) in S;

      then

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

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

      hence thesis;

    end;

    theorem :: MESFUNC6:80

    

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

    proof

      assume

       A1: ( dom f) = A;

       A2:

      now

        let r be Real;

        now

          let x be object;

          x in (A /\ ( less_dom (f,r))) iff x in A & x in ( less_dom (f,r)) by XBOOLE_0:def 4;

          hence x in (A /\ ( less_dom (f,r))) iff x in ( less_dom (f,r)) by A1, MESFUNC1:def 11;

        end;

        then (A /\ ( less_dom (f,r))) c= ( less_dom (f,r)) & ( less_dom (f,r)) c= (A /\ ( less_dom (f,r)));

        hence (A /\ ( less_dom (f,r))) = ( less_dom (f,r));

      end;

      hereby

        assume

         A3: f is B -measurable;

        now

          let r be Real;

          ((A /\ B) /\ ( less_dom (f,r))) = (B /\ (A /\ ( less_dom (f,r)))) by XBOOLE_1: 16

          .= (B /\ ( less_dom (f,r))) by A2;

          hence ((A /\ B) /\ ( less_dom (f,r))) in S by A3, Th12;

        end;

        hence f is (A /\ B) -measurable by Th12;

      end;

      assume

       A4: f is (A /\ B) -measurable;

      now

        let r be Real;

        ((A /\ B) /\ ( less_dom (f,r))) = (B /\ (A /\ ( less_dom (f,r)))) by XBOOLE_1: 16

        .= (B /\ ( less_dom (f,r))) by A2;

        hence (B /\ ( less_dom (f,r))) in S by A4, Th12;

      end;

      hence thesis by Th12;

    end;

    theorem :: MESFUNC6:81

    (ex A be Element of S st ( dom f) = A) implies for c be Real, 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);

      let c be Real, B be Element of S;

      assume f is B -measurable;

      then f is (A /\ B) -measurable by A1, Th80;

      then

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

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

      hence thesis by A2, Th80;

    end;

    begin

    reserve X for non empty set,

S for SigmaField of X,

M for sigma_Measure of S,

f,g for PartFunc of X, REAL ,

r for Real,

E,A,B for Element of S;

    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, REAL ;

      :: MESFUNC6:def3

      func Integral (M,f) -> Element of ExtREAL equals ( Integral (M,( R_EAL f)));

      coherence ;

    end

    theorem :: MESFUNC6:82

    

     Th82: (ex A be Element of S st A = ( dom f) & f is A -measurable) & f is nonnegative implies ( Integral (M,f)) = ( integral+ (M,( R_EAL f))) by MESFUNC5: 88;

    theorem :: MESFUNC6:83

    f is_simple_func_in S & f is nonnegative implies ( Integral (M,f)) = ( integral+ (M,( R_EAL f))) & ( Integral (M,f)) = ( integral' (M,( R_EAL f)))

    proof

      assume that

       A1: f is_simple_func_in S and

       A2: f is nonnegative;

      

       A3: ( R_EAL f) is_simple_func_in S by A1, Th49;

      then

      reconsider A = ( dom ( R_EAL f)) as Element of S by MESFUNC5: 37;

      ( R_EAL f) is A -measurable by A3, MESFUNC2: 34;

      then f is A -measurable;

      hence ( Integral (M,f)) = ( integral+ (M,( R_EAL f))) by A2, Th82;

      hence thesis by A2, A3, MESFUNC5: 77;

    end;

    theorem :: MESFUNC6:84

    (ex A be Element of S st A = ( dom f) & f is A -measurable) & f is nonnegative implies 0 <= ( Integral (M,f)) by MESFUNC5: 90;

    theorem :: MESFUNC6:85

    (ex E be Element of S st E = ( dom f) & f is E -measurable) & f is nonnegative & A misses B implies ( Integral (M,(f | (A \/ B)))) = (( Integral (M,(f | A))) + ( Integral (M,(f | B)))) by MESFUNC5: 91;

    theorem :: MESFUNC6:86

    (ex E be Element of S st E = ( dom f) & f is E -measurable) & f is nonnegative implies 0 <= ( Integral (M,(f | A))) by MESFUNC5: 92;

    theorem :: MESFUNC6:87

    (ex E be Element of S st E = ( dom f) & f is E -measurable) & f is nonnegative & A c= B implies ( Integral (M,(f | A))) <= ( Integral (M,(f | B))) by MESFUNC5: 93;

    theorem :: MESFUNC6:88

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

    theorem :: MESFUNC6:89

    E = ( dom f) & f is E -measurable & (M . A) = 0 implies ( Integral (M,(f | (E \ A)))) = ( Integral (M,f)) by MESFUNC5: 95;

    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, REAL ;

      :: MESFUNC6:def4

      pred f is_integrable_on M means ( R_EAL f) is_integrable_on M;

    end

    theorem :: MESFUNC6:90

    f is_integrable_on M implies -infty < ( Integral (M,f)) & ( Integral (M,f)) < +infty by MESFUNC5: 96;

    theorem :: MESFUNC6:91

    f is_integrable_on M implies (f | A) is_integrable_on M by MESFUNC5: 97;

    theorem :: MESFUNC6:92

    f is_integrable_on M & A misses B implies ( Integral (M,(f | (A \/ B)))) = (( Integral (M,(f | A))) + ( Integral (M,(f | B)))) by MESFUNC5: 98;

    theorem :: MESFUNC6:93

    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)))) by MESFUNC5: 99;

    theorem :: MESFUNC6:94

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

    proof

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

      then

      consider A be Element of S such that

       A1: A = ( dom f) and

       A2: f is A -measurable;

      ( R_EAL f) is A -measurable by A2;

      then ( R_EAL f) is_integrable_on M iff |.( R_EAL f).| is_integrable_on M by A1, MESFUNC5: 100;

      then f is_integrable_on M iff ( R_EAL ( abs f)) is_integrable_on M by Th1;

      hence thesis;

    end;

    theorem :: MESFUNC6:95

    f is_integrable_on M implies |.( Integral (M,f)).| <= ( Integral (M,( abs f)))

    proof

      assume f is_integrable_on M;

      then ( R_EAL f) is_integrable_on M;

      then |.( Integral (M,f)).| <= ( Integral (M, |.( R_EAL f).|)) by MESFUNC5: 101;

      hence thesis by Th1;

    end;

    theorem :: MESFUNC6:96

    (ex A be Element of S st A = ( dom f) & f is A -measurable) & ( dom f) = ( dom g) & g is_integrable_on M & (for x be Element of X st x in ( dom f) holds |.(f . x) qua Complex.| <= (g . x)) implies f is_integrable_on M & ( Integral (M,( abs f))) <= ( Integral (M,g))

    proof

      assume that

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

       A2: ( dom f) = ( dom g) and

       A3: g is_integrable_on M and

       A4: for x be Element of X st x in ( dom f) holds |.(f . x) qua Complex.| <= (g . x);

      

       A5: ( R_EAL g) is_integrable_on M by A3;

       A6:

      now

        let x be Element of X;

        

         A7: |.(f . x) qua Complex.| = |.(( R_EAL f) . x).| by EXTREAL1: 12;

        assume x in ( dom ( R_EAL f));

        hence |.(( R_EAL f) . x).| <= (( R_EAL g) . x) by A4, A7;

      end;

      consider A be Element of S such that

       A8: A = ( dom f) and

       A9: f is A -measurable by A1;

      ( R_EAL f) is A -measurable by A9;

      then ( R_EAL f) is_integrable_on M & ( Integral (M, |.( R_EAL f).|)) <= ( Integral (M,( R_EAL g))) by A2, A8, A5, A6, MESFUNC5: 102;

      hence thesis by Th1;

    end;

    theorem :: MESFUNC6:97

    ( dom f) in S & 0 <= r & (for x be object st x in ( dom f) holds (f . x) = r) implies ( Integral (M,f)) = (r * (M . ( dom f)))

    proof

      assume that

       A1: ( dom f) in S and

       A2: 0 <= r and

       A3: for x be object st x in ( dom f) holds (f . x) = r;

      

       A4: for x be object st x in ( dom ( R_EAL f)) holds 0. <= (( R_EAL f) . x) by A2, A3;

      reconsider A = ( dom ( R_EAL f)) as Element of S by A1;

      

       A5: ( R_EAL f) is A -measurable by A3, Th2, MESFUNC2: 34;

      (r * (M . ( dom ( R_EAL f)))) = ( integral' (M,( R_EAL f))) & ( R_EAL f) is_simple_func_in S by A1, A2, A3, Th2, MESFUNC5: 104;

      then ( integral+ (M,( R_EAL f))) = (r * (M . ( dom ( R_EAL f)))) by A4, MESFUNC5: 77, SUPINF_2: 52;

      hence thesis by A4, A5, MESFUNC5: 88, SUPINF_2: 52;

    end;

    theorem :: MESFUNC6:98

    f is_integrable_on M & g is_integrable_on M & f is nonnegative & g is nonnegative implies (f + g) is_integrable_on M

    proof

      assume that

       A1: f is_integrable_on M & g is_integrable_on M and

       A2: f is nonnegative & g is nonnegative;

      ( R_EAL f) is_integrable_on M & ( R_EAL g) is_integrable_on M by A1;

      then (( R_EAL f) + ( R_EAL g)) is_integrable_on M by A2, MESFUNC5: 106;

      then ( R_EAL (f + g)) is_integrable_on M by Th23;

      hence thesis;

    end;

    theorem :: MESFUNC6:99

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

    proof

      assume f is_integrable_on M & g is_integrable_on M;

      then ( R_EAL f) is_integrable_on M & ( R_EAL g) is_integrable_on M;

      then ( dom (( R_EAL f) + ( R_EAL g))) in S by MESFUNC5: 107;

      then ( dom ( R_EAL (f + g))) in S by Th23;

      hence thesis;

    end;

    theorem :: MESFUNC6:100

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

    proof

      assume f is_integrable_on M & g is_integrable_on M;

      then ( R_EAL f) is_integrable_on M & ( R_EAL g) is_integrable_on M;

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

      then ( R_EAL (f + g)) is_integrable_on M by Th23;

      hence thesis;

    end;

    theorem :: MESFUNC6:101

    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 f is_integrable_on M & g is_integrable_on M;

      then ( R_EAL f) is_integrable_on M & ( R_EAL g) is_integrable_on M;

      then

      consider E be Element of S such that

       A1: E = (( dom ( R_EAL f)) /\ ( dom ( R_EAL g))) & ( Integral (M,(( R_EAL f) + ( R_EAL g)))) = (( Integral (M,(( R_EAL f) | E))) + ( Integral (M,(( R_EAL g) | E)))) by MESFUNC5: 109;

      take E;

      thus thesis by A1, Th23;

    end;

    theorem :: MESFUNC6:102

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

    proof

      assume f is_integrable_on M;

      then

       A1: ( R_EAL f) is_integrable_on M;

      then (r (#) ( R_EAL f)) is_integrable_on M by MESFUNC5: 110;

      then

       A2: ( R_EAL (r (#) f)) is_integrable_on M by Th20;

      ( Integral (M,(r (#) ( R_EAL f)))) = (r * ( Integral (M,( R_EAL f)))) by A1, MESFUNC5: 110;

      hence thesis by A2, Th20;

    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, REAL ;

      let B be Element of S;

      :: MESFUNC6:def5

      func Integral_on (M,B,f) -> Element of ExtREAL equals ( Integral (M,(f | B)));

      coherence ;

    end

    theorem :: MESFUNC6:103

    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 & g is_integrable_on M and

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

      

       A3: ( dom (f + g)) = ( dom ( R_EAL (f + g)))

      .= ( dom (( R_EAL f) + ( R_EAL g))) by Th23;

      

       A4: ( R_EAL f) is_integrable_on M & ( R_EAL g) is_integrable_on M by A1;

      then (( R_EAL f) + ( R_EAL g)) is_integrable_on M by A2, A3, MESFUNC5: 111;

      then

       A5: ( R_EAL (f + g)) is_integrable_on M by Th23;

      ( Integral_on (M,B,(( R_EAL f) + ( R_EAL g)))) = (( Integral_on (M,B,( R_EAL f))) + ( Integral_on (M,B,( R_EAL g)))) by A2, A4, A3, MESFUNC5: 111;

      hence thesis by A5, Th23;

    end;

    theorem :: MESFUNC6:104

    f is_integrable_on M implies (f | B) is_integrable_on M & ( Integral_on (M,B,(r (#) f))) = (r * ( Integral_on (M,B,f)))

    proof

      assume f is_integrable_on M;

      then

       A1: ( R_EAL f) is_integrable_on M;

      then ( Integral_on (M,B,(r (#) ( R_EAL f)))) = (r * ( Integral_on (M,B,( R_EAL f)))) by MESFUNC5: 112;

      then

       A2: ( Integral_on (M,B,( R_EAL (r (#) f)))) = (r * ( Integral_on (M,B,( R_EAL f)))) by Th20;

      ( R_EAL (f | B)) is_integrable_on M by A1, MESFUNC5: 112;

      hence thesis by A2;

    end;