random_1.miz



    begin

    theorem :: RANDOM_1:1

    

     Th1: for X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f be PartFunc of X, ExtREAL , E be Element of S, a be Real st f is_integrable_on M & E c= ( dom f) & (M . E) < +infty & (for x be Element of X st x in E holds a <= (f . x)) holds (a qua ExtReal * (M . E)) <= ( Integral (M,(f | E)))

    proof

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

      assume that

       A1: f is_integrable_on M and

       A2: E c= ( dom f) and

       A3: (M . E) < +infty and

       A4: for x be Element of X st x in E holds a <= (f . x);

      set C = ( chi (E,X));

      

       A5: (f | E) is_integrable_on M by A1, MESFUNC5: 97;

      for x be Element of X st x in ( dom (a (#) (C | E))) holds ((a (#) (C | E)) . x) <= ((f | E) . x)

      proof

        let x be Element of X;

        assume

         A6: x in ( dom (a (#) (C | E)));

        then

         A7: x in ( dom (C | E)) by MESFUNC1:def 6;

        then x in (( dom C) /\ E) by RELAT_1: 61;

        then

         A8: x in E by XBOOLE_0:def 4;

        then a <= (f . x) by A4;

        then

         A9: a <= ((f | E) . x) by A8, FUNCT_1: 49;

        ((a (#) (C | E)) . x) = (a * ((C | E) . x)) by A6, MESFUNC1:def 6

        .= (a * (C . x)) by A7, FUNCT_1: 47

        .= (a * 1. ) by A8, FUNCT_3:def 3;

        hence thesis by A9, XXREAL_3: 81;

      end;

      then

       A10: ((f | E) - (a (#) (C | E))) is nonnegative by MESFUNC7: 1;

      ( dom (a (#) (C | E))) = ( dom (C | E)) by MESFUNC1:def 6;

      then ( dom (a (#) (C | E))) = (( dom C) /\ E) by RELAT_1: 61;

      then ( dom (a (#) (C | E))) = (X /\ E) by FUNCT_3:def 3;

      then

       A11: ( dom (a (#) (C | E))) = E by XBOOLE_1: 28;

      E = (E /\ E);

      then

       A12: ( Integral (M,(C | E))) = (M . E) by A3, MESFUNC7: 25;

      reconsider a as Real;

      ( chi (E,X)) is_integrable_on M by A3, MESFUNC7: 24;

      then

       A13: (C | E) is_integrable_on M by MESFUNC5: 97;

      then (a (#) (C | E)) is_integrable_on M by MESFUNC5: 110;

      then

      consider E1 be Element of S such that

       A14: E1 = (( dom (f | E)) /\ ( dom (a (#) (C | E)))) and

       A15: ( Integral (M,((a (#) (C | E)) | E1))) <= ( Integral (M,((f | E) | E1))) by A5, A10, MESFUNC7: 3;

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

      then ( dom (f | E)) = E by A2, XBOOLE_1: 28;

      then ((a (#) (C | E)) | E1) = (a (#) (C | E)) & ((f | E) | E1) = (f | E) by A14, A11;

      hence thesis by A13, A15, A12, MESFUNC5: 110;

    end;

    theorem :: RANDOM_1:2

    

     Th2: for X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f be PartFunc of X, REAL , E be Element of S, a be Real st f is_integrable_on M & E c= ( dom f) & (M . E) < +infty & (for x be Element of X st x in E holds a <= (f . x)) holds (a qua ExtReal * (M . E)) <= ( Integral (M,(f | E))) by Th1;

    theorem :: RANDOM_1:3

    

     Th3: for X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f be PartFunc of X, ExtREAL , E be Element of S, a be Real st f is_integrable_on M & E c= ( dom f) & (M . E) < +infty & (for x be Element of X st x in E holds (f . x) <= a) holds ( Integral (M,(f | E))) <= (a qua ExtReal * (M . E))

    proof

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

      assume that

       A1: f is_integrable_on M and

       A2: E c= ( dom f) and

       A3: (M . E) < +infty and

       A4: for x be Element of X st x in E holds (f . x) <= a;

      set C = ( chi (E,X));

      

       A5: (f | E) is_integrable_on M by A1, MESFUNC5: 97;

      ( dom (a (#) (C | E))) = ( dom (C | E)) by MESFUNC1:def 6;

      then ( dom (a (#) (C | E))) = (( dom C) /\ E) by RELAT_1: 61;

      then ( dom (a (#) (C | E))) = (X /\ E) by FUNCT_3:def 3;

      then

       A6: ( dom (a (#) (C | E))) = E by XBOOLE_1: 28;

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

      then

       A7: ( dom (f | E)) = E by A2, XBOOLE_1: 28;

      for x be Element of X st x in ( dom (f | E)) holds ((f | E) . x) <= ((a (#) (C | E)) . x)

      proof

        let x be Element of X;

        assume

         A8: x in ( dom (f | E));

        then

         A9: x in ( dom (C | E)) by A7, A6, MESFUNC1:def 6;

        then x in (( dom C) /\ E) by RELAT_1: 61;

        then

         A10: x in E by XBOOLE_0:def 4;

        then (f . x) <= a by A4;

        then

         A11: ((f | E) . x) <= a by A10, FUNCT_1: 49;

        ((a (#) (C | E)) . x) = (a * ((C | E) . x)) by A7, A6, A8, MESFUNC1:def 6

        .= (a * (C . x)) by A9, FUNCT_1: 47

        .= (a * 1. ) by A10, FUNCT_3:def 3;

        hence thesis by A11, XXREAL_3: 81;

      end;

      then

       A12: ((a (#) (C | E)) - (f | E)) is nonnegative by MESFUNC7: 1;

      ( dom (a (#) (C | E))) = ( dom (C | E)) by MESFUNC1:def 6;

      then ( dom (a (#) (C | E))) = (( dom C) /\ E) by RELAT_1: 61;

      then ( dom (a (#) (C | E))) = (X /\ E) by FUNCT_3:def 3;

      then

       A13: ( dom (a (#) (C | E))) = E by XBOOLE_1: 28;

      E = (E /\ E);

      then

       A14: ( Integral (M,(C | E))) = (M . E) by A3, MESFUNC7: 25;

      ( chi (E,X)) is_integrable_on M by A3, MESFUNC7: 24;

      then

       A15: (C | E) is_integrable_on M by MESFUNC5: 97;

      then (a (#) (C | E)) is_integrable_on M by MESFUNC5: 110;

      then

      consider E1 be Element of S such that

       A16: E1 = (( dom (f | E)) /\ ( dom (a (#) (C | E)))) and

       A17: ( Integral (M,((f | E) | E1))) <= ( Integral (M,((a (#) (C | E)) | E1))) by A5, A12, MESFUNC7: 3;

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

      then ( dom (f | E)) = E by A2, XBOOLE_1: 28;

      then ((a (#) (C | E)) | E1) = (a (#) (C | E)) & ((f | E) | E1) = (f | E) by A16, A13;

      hence thesis by A15, A17, A14, MESFUNC5: 110;

    end;

    theorem :: RANDOM_1:4

    for X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f be PartFunc of X, REAL , E be Element of S, a be Real st f is_integrable_on M & E c= ( dom f) & (M . E) < +infty & (for x be Element of X st x in E holds (f . x) <= a) holds ( Integral (M,(f | E))) <= (a qua ExtReal * (M . E)) by Th3;

    

     Lm1: for X be non empty set, S be SigmaField of X, f be PartFunc of X, REAL , M be sigma_Measure of S, F be Finite_Sep_Sequence of S, a be FinSequence of REAL , x be FinSequence of ExtREAL st f is_simple_func_in S & ( dom f) <> {} & f is nonnegative & ( dom f) = ( union ( rng F)) & ( dom F) = ( dom a) & (for n be Nat st n in ( dom F) holds for x be object st x in (F . n) holds (f . x) = (a . n)) & ( dom x) = ( dom F) & (for n be Nat st n in ( dom x) holds (x . n) = ((a . n) qua ExtReal * ((M * F) . n))) holds ( Integral (M,f)) = ( Sum x)

    proof

      let X be non empty set, S be SigmaField of X, f be PartFunc of X, REAL , M be sigma_Measure of S, F be Finite_Sep_Sequence of S, a be FinSequence of REAL , x be FinSequence of ExtREAL ;

      assume that

       A1: f is_simple_func_in S and

       A2: ( dom f) <> {} and

       A3: f is nonnegative and

       A4: ( dom f) = ( union ( rng F)) & ( dom F) = ( dom a) & for n be Nat st n in ( dom F) holds for x be object st x in (F . n) holds (f . x) = (a . n) and

       A5: ( dom x) = ( dom F) and

       A6: for n be Nat st n in ( dom x) holds (x . n) = ((a . n) qua ExtReal * ((M * F) . n));

      

       A7: ( R_EAL f) is_simple_func_in S & for x be object st x in ( dom ( R_EAL f)) holds 0 <= (( R_EAL f) . x) by A1, A3, MESFUNC6: 49, MESFUNC6: 51;

      reconsider a0 = a as FinSequence of ExtREAL by MESFUNC3: 11;

      

       A8: (F,a0) are_Re-presentation_of ( R_EAL f) by A4, MESFUNC3:def 1;

      

       A9: for n be Nat st n in ( dom x) holds (x . n) = ((a0 . n) * ((M * F) . n)) by A6;

      

      thus ( Integral (M,f)) = ( integral' (M,( R_EAL f))) by A1, A3, MESFUNC6: 83

      .= ( integral (M,( R_EAL f))) by A2, MESFUNC5:def 14

      .= ( Sum x) by A2, A3, A5, A7, A8, A9, MESFUNC4: 3;

    end;

    

     Lm2: for X be non empty set, S be SigmaField of X, f be PartFunc of X, REAL st f is_simple_func_in S holds ex F be Finite_Sep_Sequence of S, a be FinSequence of REAL st ( dom f) = ( union ( rng F)) & ( dom F) = ( dom a) & for n be Nat st n in ( dom F) holds for x be set st x in (F . n) holds (f . x) = (a . n)

    proof

      let X be non empty set;

      let S be SigmaField of X;

      let f be PartFunc of X, REAL ;

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

      defpred P[ Nat, Real] means for x be set st x in (F . $1) holds $2 = (f . x);

      

       A3: for k be Nat st k in ( Seg ( len F)) holds ex y be Element of REAL st P[k, y]

      proof

        let k be Nat;

        assume k in ( Seg ( len F));

        then

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

        then

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

        per cases ;

          suppose

           A6: (F . k) = {} ;

          take ( In ( 0 , REAL ));

          thus thesis by A6;

        end;

          suppose (F . k) <> {} ;

          then

          consider x1 be object such that

           A7: x1 in (F . k) by XBOOLE_0:def 1;

          reconsider fx1 = (f . x1) as Element of REAL by XREAL_0:def 1;

          take fx1;

          ( rng F) c= ( bool X) by XBOOLE_1: 1;

          hence thesis by A2, A4, A5, A7;

        end;

      end;

      consider a be FinSequence of REAL such that

       A8: ( dom a) = ( Seg ( len F)) & for k be Nat st k in ( Seg ( len F)) holds P[k, (a . k)] from FINSEQ_1:sch 5( A3);

      take F, a;

      for n be Nat st n in ( dom F) holds for x be set st x in (F . n) holds (a . n) = (f . x)

      proof

        let n be Nat;

        assume n in ( dom F);

        then n in ( Seg ( len F)) by FINSEQ_1:def 3;

        hence thesis by A8;

      end;

      hence thesis by A1, A8, FINSEQ_1:def 3;

    end;

    

     Lm3: for X be non empty set, S be SigmaField of X, f be PartFunc of X, REAL st f is_simple_func_in S holds ( rng f) is real-bounded

    proof

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

      assume f is_simple_func_in S;

      then

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

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

       A2: ( dom F) = ( dom a) and

       A3: for n be Nat st n in ( dom F) holds for x be set st x in (F . n) holds (f . x) = (a . n) by Lm2;

      ( rng f) c= ( rng a)

      proof

        let y be object;

        assume y in ( rng f);

        then

        consider x be object such that

         A4: x in ( dom f) and

         A5: y = (f . x) by FUNCT_1:def 3;

        consider z be set such that

         A6: x in z and

         A7: z in ( rng F) by A1, A4, TARSKI:def 4;

        consider n be object such that

         A8: n in ( dom F) and

         A9: z = (F . n) by A7, FUNCT_1:def 3;

        (f . x) = (a . n) by A3, A6, A8, A9;

        hence y in ( rng a) by A2, A5, A8, FUNCT_1:def 3;

      end;

      hence thesis by RCOMP_1: 10;

    end;

    

     Lm4: for X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f be PartFunc of X, REAL st ( dom f) <> {} & ( rng f) is real-bounded & (M . ( dom f)) < +infty & ex E be Element of S st E = ( dom f) & f is E -measurable holds f is_integrable_on M

    proof

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

      assume that

       A1: ( dom f) <> {} and

       A2: ( rng f) is real-bounded and

       A3: (M . ( dom f)) < +infty and

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

      consider E be Element of S such that

       A5: E = ( dom f) and

       A6: f is E -measurable by A4;

      

       A7: (( dom ( R_EAL f)) /\ ( dom ( chi (E,X)))) = (E /\ X) by A5, FUNCT_3:def 3;

      then

       A8: ( chi (E,X)) is real-valued & (( dom ( R_EAL f)) /\ ( dom ( chi (E,X)))) = E by MESFUNC2: 28, XBOOLE_1: 28;

      

       A9: ( dom (( R_EAL f) (#) ( chi (E,X)))) = (( dom ( R_EAL f)) /\ ( dom ( chi (E,X)))) by MESFUNC1:def 5

      .= E by A7, XBOOLE_1: 28;

       A10:

      now

        let x be object;

        assume

         A11: x in ( dom f);

        then ((( R_EAL f) (#) ( chi (E,X))) . x) = ((( R_EAL f) . x) * (( chi (E,X)) . x)) by A5, A9, MESFUNC1:def 5;

        

        then ((( R_EAL f) (#) ( chi (E,X))) . x) = ((( R_EAL f) . x) * 1) by A5, A11, FUNCT_3:def 3

        .= (f . x) by XXREAL_3: 81;

        hence (((( R_EAL f) (#) ( chi (E,X))) | E) . x) = (f . x) by A9;

      end;

      

       A12: ( R_EAL f) is E -measurable by A6;

      

       A13: ( rng ( R_EAL f)) is non empty Subset of ExtREAL by A1, RELAT_1: 42;

      ( dom ((( R_EAL f) (#) ( chi (E,X))) | E)) = ( dom f) by A5, A9;

      then

       A14: ((( R_EAL f) (#) ( chi (E,X))) | E) = f by A10, FUNCT_1: 2;

      ( chi (E,X)) is_integrable_on M by A3, A5, MESFUNC7: 24;

      then ((( R_EAL f) (#) ( chi (E,X))) | E) is_integrable_on M by A2, A13, A12, A8, MESFUNC7: 17;

      hence thesis by A14;

    end;

    

     Lm5: for X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f be PartFunc of X, REAL st f is_simple_func_in S & ( dom f) <> {} & ( dom f) in S & (M . ( dom f)) < +infty holds f is_integrable_on M

    proof

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

      assume

       A1: f is_simple_func_in S;

      then ( rng f) is real-bounded by Lm3;

      hence thesis by A1, Lm4, MESFUNC6: 50;

    end;

    begin

    reserve Omega for non empty set;

    reserve r for Real;

    reserve Sigma for SigmaField of Omega;

    reserve P for Probability of Sigma;

    reserve E for finite non empty set;

    notation

      let E be non empty set;

      synonym Trivial-SigmaField (E) for bool E;

    end

    definition

      let E be non empty set;

      :: original: Trivial-SigmaField

      redefine

      func Trivial-SigmaField (E) -> SigmaField of E ;

      correctness by PROB_1: 40;

    end

    

     Lm6: for Omega be non empty finite set, f be PartFunc of Omega, REAL holds ex F be Finite_Sep_Sequence of ( Trivial-SigmaField Omega) st ( dom f) = ( union ( rng F)) & ( dom F) = ( dom ( canFS ( dom f))) & (for k be Nat st k in ( dom F) holds (F . k) = {(( canFS ( dom f)) . k)}) & for n be Nat holds for x,y be Element of Omega st n in ( dom F) & x in (F . n) & y in (F . n) holds (f . x) = (f . y)

    proof

      let Omega be non empty finite set, f be PartFunc of Omega, REAL ;

      set Sigma = ( Trivial-SigmaField Omega);

      set D = ( dom f);

      defpred P[ Nat, set] means $2 = {(( canFS D) . $1)};

      set L = ( len ( canFS D));

      

       A1: for k be Nat st k in ( Seg L) holds ex x be Element of ( bool Omega) st P[k, x]

      proof

        let k be Nat;

        assume

         A2: k in ( Seg L);

        take {(( canFS D) . k)};

        k in ( dom ( canFS D)) by A2, FINSEQ_1:def 3;

        then (( canFS D) . k) in ( rng ( canFS D)) by FUNCT_1: 3;

        then (( canFS D) . k) in D;

        hence thesis by ZFMISC_1: 31;

      end;

      consider F be FinSequence of ( bool Omega) such that

       A3: ( dom F) = ( Seg L) & for k be Nat st k in ( Seg L) holds P[k, (F . k)] from FINSEQ_1:sch 5( A1);

      now

        let i,j be Nat;

        assume that

         A4: i in ( dom F) & j in ( dom F) and

         A5: i <> j;

        i in ( dom ( canFS D)) & j in ( dom ( canFS D)) by A3, A4, FINSEQ_1:def 3;

        then

         A6: (( canFS D) . i) <> (( canFS D) . j) by A5, FUNCT_1:def 4;

        (F . i) = {(( canFS D) . i)} & (F . j) = {(( canFS D) . j)} by A3, A4;

        hence (F . i) misses (F . j) by A6, ZFMISC_1: 11;

      end;

      then

      reconsider F as Finite_Sep_Sequence of Sigma by MESFUNC3: 4;

      now

        let x be object;

        assume x in ( rng ( canFS D));

        then

        consider n be object such that

         A7: n in ( dom ( canFS D)) and

         A8: x = (( canFS D) . n) by FUNCT_1:def 3;

        

         A9: n in ( Seg L) by A7, FINSEQ_1:def 3;

        reconsider n as Element of NAT by A7;

        n in ( dom F) by A3, A7, FINSEQ_1:def 3;

        then

         A10: (F . n) in ( rng F) by FUNCT_1:def 3;

        x in {(( canFS D) . n)} by A8, TARSKI:def 1;

        then x in (F . n) by A3, A9;

        hence x in ( union ( rng F)) by A10, TARSKI:def 4;

      end;

      then

       A11: ( rng ( canFS D)) c= ( union ( rng F));

      take F;

      

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

      proof

        let n be Nat;

        let x,y be Element of Omega;

        assume that

         A13: n in ( dom F) and

         A14: x in (F . n) and

         A15: y in (F . n);

        

         A16: (F . n) = {(( canFS D) . n)} by A3, A13;

        

        hence (f . x) = (f . (( canFS D) . n)) by A14, TARSKI:def 1

        .= (f . y) by A15, A16, TARSKI:def 1;

      end;

      now

        let x be object;

        assume x in ( union ( rng F));

        then

        consider y be set such that

         A17: x in y and

         A18: y in ( rng F) by TARSKI:def 4;

        consider n be object such that

         A19: n in ( dom F) and

         A20: y = (F . n) by A18, FUNCT_1:def 3;

        reconsider n as Element of NAT by A19;

        (F . n) = {(( canFS D) . n)} by A3, A19;

        then

         A21: x = (( canFS D) . n) by A17, A20, TARSKI:def 1;

        n in ( dom ( canFS D)) by A3, A19, FINSEQ_1:def 3;

        hence x in ( rng ( canFS D)) by A21, FUNCT_1:def 3;

      end;

      then ( union ( rng F)) c= ( rng ( canFS D));

      then ( union ( rng F)) = ( rng ( canFS D)) by A11;

      hence thesis by A3, A12, FINSEQ_1:def 3, FUNCT_2:def 3;

    end;

    theorem :: RANDOM_1:5

    for Omega be non empty finite set, f be PartFunc of Omega, REAL holds ex F be Finite_Sep_Sequence of ( Trivial-SigmaField Omega), s be FinSequence of ( dom f) st ( dom f) = ( union ( rng F)) & ( dom F) = ( dom s) & s is one-to-one & ( rng s) = ( dom f) & ( len s) = ( card ( dom f)) & (for k be Nat st k in ( dom F) holds (F . k) = {(s . k)}) & for n be Nat holds for x,y be Element of Omega st n in ( dom F) & x in (F . n) & y in (F . n) holds (f . x) = (f . y)

    proof

      let Omega be non empty finite set, f be PartFunc of Omega, REAL ;

      set Sigma = ( Trivial-SigmaField Omega);

      set D = ( dom f);

      set s = ( canFS D);

      

       A1: ( len s) = ( card ( dom f)) by FINSEQ_1: 93;

      (ex F be Finite_Sep_Sequence of Sigma st ( dom f) = ( union ( rng F)) & ( dom F) = ( dom ( canFS D)) & (for k be Nat st k in ( dom F) holds (F . k) = {(( canFS D) . k)}) & for n be Nat holds for x,y be Element of Omega st n in ( dom F) & x in (F . n) & y in (F . n) holds (f . x) = (f . y)) & ( rng s) = ( dom f) by Lm6, FUNCT_2:def 3;

      hence thesis by A1;

    end;

    theorem :: RANDOM_1:6

    

     Th6: for Omega be non empty finite set, f be PartFunc of Omega, REAL holds f is_simple_func_in ( Trivial-SigmaField Omega) & ( dom f) is Element of ( Trivial-SigmaField Omega)

    proof

      let Omega be non empty finite set, f be PartFunc of Omega, REAL ;

      set Sigma = ( Trivial-SigmaField Omega), D = ( dom f);

      ex F be Finite_Sep_Sequence of Sigma st ( dom f) = ( union ( rng F)) & ( dom F) = ( dom ( canFS D)) & (for k be Nat st k in ( dom F) holds (F . k) = {(( canFS D) . k)}) & for n be Nat holds for x,y be Element of Omega st n in ( dom F) & x in (F . n) & y in (F . n) holds (f . x) = (f . y) by Lm6;

      hence thesis;

    end;

    theorem :: RANDOM_1:7

    for Omega be non empty finite set, M be sigma_Measure of ( Trivial-SigmaField Omega), f be PartFunc of Omega, REAL st ( dom f) <> {} & (M . ( dom f)) < +infty holds f is_integrable_on M by Lm5, Th6;

    

     Lm7: for Omega be non empty set, Sigma be SigmaField of Omega, M be sigma_Measure of Sigma, A,B be set st A in Sigma & B in Sigma & A c= B & (M . B) < +infty holds (M . A) in REAL

    proof

      let Omega be non empty set, Sigma be SigmaField of Omega, M be sigma_Measure of Sigma, A,B be set;

      assume A in Sigma & B in Sigma & A c= B & (M . B) < +infty ;

      then (M . A) <> -infty & (M . A) <> +infty by MEASURE1: 31, MEASURE1:def 2;

      hence thesis by XXREAL_0: 14;

    end;

    

     Lm8: for Omega be non empty finite set, f be PartFunc of Omega, REAL holds (f * ( canFS ( dom f))) is FinSequence of REAL

    proof

      let Omega be non empty finite set, f be PartFunc of Omega, REAL ;

      ( rng ( canFS ( dom f))) c= ( dom f);

      then

       A1: (f * ( canFS ( dom f))) is FinSequence by FINSEQ_1: 16;

      ( rng (f * ( canFS ( dom f)))) c= REAL ;

      hence (f * ( canFS ( dom f))) is FinSequence of REAL by A1, FINSEQ_1:def 4;

    end;

    

     Lm9: for Omega be non empty finite set, f be PartFunc of Omega, REAL holds ( dom (f * ( canFS ( dom f)))) = ( dom ( canFS ( dom f)))

    proof

      let Omega be non empty finite set, f be PartFunc of Omega, REAL ;

      ( rng ( canFS ( dom f))) c= ( dom f);

      hence ( dom (f * ( canFS ( dom f)))) = ( dom ( canFS ( dom f))) by RELAT_1: 27;

    end;

    theorem :: RANDOM_1:8

    

     Th8: for Omega be non empty finite set, f be PartFunc of Omega, REAL holds ex X be Element of ( Trivial-SigmaField Omega) st ( dom f) = X & f is X -measurable

    proof

      let Omega be non empty finite set, f be PartFunc of Omega, REAL ;

      set Sigma = ( Trivial-SigmaField Omega);

      reconsider X = ( dom f) as Element of Sigma;

      take X;

      thus thesis by Th6, MESFUNC6: 50;

    end;

    reconsider jj = 1 as Real;

    

     Lm10: for Omega be non empty finite set, M be sigma_Measure of ( Trivial-SigmaField Omega), f be Function of Omega, REAL st (M . Omega) < +infty holds ex x be FinSequence of ExtREAL st ( len x) = ( card Omega) & (for n be Nat st n in ( dom x) holds (x . n) = ((f . (( canFS Omega) . n)) * (M . {(( canFS Omega) . n)}))) & ( Integral (M,f)) = ( Sum x)

    proof

      let Omega be non empty finite set, M be sigma_Measure of ( Trivial-SigmaField Omega), f be Function of Omega, REAL ;

      set fm = ( max- f);

      set Dm = ( dom fm);

      reconsider am = (fm * ( canFS Dm)) as FinSequence of REAL by Lm8;

      set fp = ( max+ f);

      set Dp = ( dom fp);

      reconsider ap = (fp * ( canFS Dp)) as FinSequence of REAL by Lm8;

      set Sigma = ( Trivial-SigmaField Omega), D = ( dom f);

      consider F be Finite_Sep_Sequence of Sigma such that ( dom f) = ( union ( rng F)) and

       A1: ( dom F) = ( dom ( canFS D)) and

       A2: for k be Nat st k in ( dom F) holds (F . k) = {(( canFS D) . k)} and for n be Nat holds for x,y be Element of Omega st n in ( dom F) & x in (F . n) & y in (F . n) holds (f . x) = (f . y) by Lm6;

      set L = ( len F);

      consider Fp be Finite_Sep_Sequence of Sigma such that

       A3: ( dom fp) = ( union ( rng Fp)) and

       A4: ( dom Fp) = ( dom ( canFS Dp)) and

       A5: for k be Nat st k in ( dom Fp) holds (Fp . k) = {(( canFS Dp) . k)} and for n be Nat holds for x,y be Element of Omega st n in ( dom Fp) & x in (Fp . n) & y in (Fp . n) holds (fp . x) = (fp . y) by Lm6;

      defpred Pp[ Nat, set] means $2 = ((ap . $1) * ((M * Fp) . $1));

      

       A6: for k be Nat st k in ( Seg L) holds ex x be Element of ExtREAL st Pp[k, x];

      consider xp be FinSequence of ExtREAL such that

       A7: ( dom xp) = ( Seg L) & for k be Nat st k in ( Seg L) holds Pp[k, (xp . k)] from FINSEQ_1:sch 5( A6);

      

       A8: ( dom Fp) = ( dom ap) by A4, Lm9;

      

       A9: for n be Nat st n in ( dom Fp) holds for x be object st x in (Fp . n) holds (fp . x) = (ap . n)

      proof

        let n be Nat such that

         A10: n in ( dom Fp);

        let x be object;

        assume x in (Fp . n);

        then x in {(( canFS Dp) . n)} by A5, A10;

        then x = (( canFS Dp) . n) by TARSKI:def 1;

        hence (fp . x) = (ap . n) by A8, A10, FUNCT_1: 12;

      end;

      reconsider a = (f * ( canFS D)) as FinSequence of REAL by Lm8;

      

       A11: (( - jj) * ( Integral (M,fm))) = (( - jj qua ExtReal) * ( Integral (M,fm)))

      .= ( - (1 * ( Integral (M,fm)))) by XXREAL_3: 92

      .= ( - ( Integral (M,fm))) by XXREAL_3: 81;

      defpred PX[ Nat, set] means $2 = ((a . $1) * ((M * F) . $1));

      

       A12: for k be Nat st k in ( Seg L) holds ex x be Element of ExtREAL st PX[k, x];

      consider x be FinSequence of ExtREAL such that

       A13: ( dom x) = ( Seg L) & for k be Nat st k in ( Seg L) holds PX[k, (x . k)] from FINSEQ_1:sch 5( A12);

      assume

       A14: (M . Omega) < +infty ;

      

       A15: for n be Nat st n in ( dom ( canFS Omega)) holds (M . {(( canFS Omega) . n)}) in REAL

      proof

        let n be Nat;

        assume n in ( dom ( canFS Omega));

        then (( canFS Omega) . n) in ( rng ( canFS Omega)) by FUNCT_1: 3;

        then

         A16: {(( canFS Omega) . n)} c= Omega by ZFMISC_1: 31;

        Omega in Sigma by MEASURE1: 7;

        hence (M . {(( canFS Omega) . n)}) in REAL by A14, A16, Lm7;

      end;

      

       A17: ( dom f) = Omega by FUNCT_2:def 1;

      then

       A18: ( dom fm) = Omega by RFUNCT_3:def 11;

      then

       A19: fm is_integrable_on M by A14, Lm5, Th6;

      

       A20: ( dom x) = ( dom F) by A13, FINSEQ_1:def 3;

      

       A21: for n be Nat st n in ( dom x) holds (x . n) = ((f . (( canFS Omega) . n)) * (M . {(( canFS Omega) . n)}))

      proof

        let n be Nat;

        assume

         A22: n in ( dom x);

        

        then

         A23: ((M * F) . n) = (M . (F . n)) by A20, FUNCT_1: 13

        .= (M . {(( canFS Omega) . n)}) by A2, A17, A20, A22;

        

         A24: (f . (( canFS D) . n)) = (a . n) by A1, A20, A22, FUNCT_1: 13;

        

        thus (x . n) = ((a . n) * ((M * F) . n)) by A13, A22

        .= ((f . (( canFS Omega) . n)) * (M . {(( canFS Omega) . n)})) by A24, A23, FUNCT_2:def 1;

      end;

      x is FinSequence of REAL

      proof

        let y be object;

        assume y in ( rng x);

        then

        consider n be Element of NAT such that

         A25: n in ( dom x) and

         A26: y = (x . n) by PARTFUN1: 3;

        reconsider z = (M . {(( canFS Omega) . n)}) as Element of REAL by A1, A17, A20, A15, A25;

        reconsider w = (f . (( canFS Omega) . n)) as Element of REAL by XREAL_0:def 1;

        (x . n) = ((f . (( canFS Omega) . n)) * (M . {(( canFS Omega) . n)})) by A21, A25

        .= (w * z) by EXTREAL1: 1;

        hence y in REAL by A26;

      end;

      then

      reconsider x1 = x as FinSequence of REAL ;

      take x;

      

       A27: fm is_simple_func_in Sigma & fm is nonnegative by Th6, MESFUNC6: 61;

      

       A28: ( dom Fp) = ( dom F) by A1, A4, RFUNCT_3:def 10;

      then

       A29: ( dom xp) = ( dom Fp) by A7, FINSEQ_1:def 3;

      

       A30: Dp = D by RFUNCT_3:def 10;

      

       A31: for n be Nat st n in ( dom xp) holds (xp . n) = ((fp . (( canFS Omega) . n)) * (M . {(( canFS Omega) . n)}))

      proof

        let n be Nat;

        assume

         A32: n in ( dom xp);

        

        then

         A33: ((M * Fp) . n) = (M . (Fp . n)) by A29, FUNCT_1: 13

        .= (M . {(( canFS Omega) . n)}) by A17, A5, A30, A29, A32;

        

         A34: (fp . (( canFS D) . n)) = (ap . n) by A4, A30, A29, A32, FUNCT_1: 13;

        

        thus (xp . n) = ((ap . n) * ((M * Fp) . n)) by A7, A32

        .= ((fp . (( canFS Omega) . n)) * (M . {(( canFS Omega) . n)})) by A34, A33, FUNCT_2:def 1;

      end;

      now

        let y be object;

        assume y in ( rng xp);

        then

        consider n be Element of NAT such that

         A35: n in ( dom xp) and

         A36: y = (xp . n) by PARTFUN1: 3;

        reconsider z = (M . {(( canFS Omega) . n)}) as Element of REAL by A17, A4, A30, A29, A15, A35;

        reconsider w = (fp . (( canFS Omega) . n)) as Element of REAL by XREAL_0:def 1;

        (xp . n) = ((fp . (( canFS Omega) . n)) * (M . {(( canFS Omega) . n)})) by A31, A35

        .= (w * z) by EXTREAL1: 1;

        hence y in REAL by A36;

      end;

      then ( rng xp) c= REAL ;

      then

      reconsider xp1 = xp as FinSequence of REAL by FINSEQ_1:def 4;

      consider Fm be Finite_Sep_Sequence of Sigma such that

       A37: ( dom fm) = ( union ( rng Fm)) and

       A38: ( dom Fm) = ( dom ( canFS Dm)) and

       A39: for k be Nat st k in ( dom Fm) holds (Fm . k) = {(( canFS Dm) . k)} and for n be Nat holds for x,y be Element of Omega st n in ( dom Fm) & x in (Fm . n) & y in (Fm . n) holds (fm . x) = (fm . y) by Lm6;

      defpred Pm[ Nat, set] means $2 = ((am . $1) * ((M * Fm) . $1));

      

       A40: for k be Nat st k in ( Seg L) holds ex x be Element of ExtREAL st Pm[k, x];

      consider xm be FinSequence of ExtREAL such that

       A41: ( dom xm) = ( Seg L) & for k be Nat st k in ( Seg L) holds Pm[k, (xm . k)] from FINSEQ_1:sch 5( A40);

      

       A42: ( dom Fm) = ( dom F) by A1, A38, RFUNCT_3:def 11;

      then

       A43: ( dom xm) = ( dom Fm) by A41, FINSEQ_1:def 3;

      

       A44: Dm = D by RFUNCT_3:def 11;

      

       A45: for n be Nat st n in ( dom xm) holds (xm . n) = ((fm . (( canFS Omega) . n)) * (M . {(( canFS Omega) . n)}))

      proof

        let n be Nat;

        assume

         A46: n in ( dom xm);

        

        then

         A47: ((M * Fm) . n) = (M . (Fm . n)) by A43, FUNCT_1: 13

        .= (M . {(( canFS Omega) . n)}) by A17, A39, A44, A43, A46;

        

        thus (xm . n) = ((am . n) * ((M * Fm) . n)) by A41, A46

        .= ((fm . (( canFS Omega) . n)) * (M . {(( canFS Omega) . n)})) by A38, A43, A18, A46, A47, FUNCT_1: 13;

      end;

      now

        let y be object;

        assume y in ( rng xm);

        then

        consider n be Element of NAT such that

         A48: n in ( dom xm) and

         A49: y = (xm . n) by PARTFUN1: 3;

        reconsider z = (M . {(( canFS Omega) . n)}) as Element of REAL by A17, A38, A44, A43, A15, A48;

        reconsider w = (fm . (( canFS Omega) . n)) as Element of REAL by XREAL_0:def 1;

        (xm . n) = ((fm . (( canFS Omega) . n)) * (M . {(( canFS Omega) . n)})) by A45, A48

        .= (w * z) by EXTREAL1: 1;

        hence y in REAL by A49;

      end;

      then ( rng xm) c= REAL ;

      then

      reconsider xm1 = xm as FinSequence of REAL by FINSEQ_1:def 4;

      

       A50: ( Sum xp) = ( Sum xp1) & ( Sum xm) = ( Sum xm1) by MESFUNC3: 2;

      ( dom fp) = Omega by A17, RFUNCT_3:def 10;

      then

       A51: fp is_integrable_on M by A14, Lm5, Th6;

      

       A52: ( dom fm) = ( dom f) by RFUNCT_3:def 11;

      then

       A53: fm is Function of Omega, REAL by A17, FUNCT_2:def 1;

      then (M . ( dom (( - 1) (#) fm))) < +infty by A14, FUNCT_2:def 1;

      then (( - 1) (#) fm) is_integrable_on M by A53, Lm5, Th6;

      then

      consider E be Element of Sigma such that

       A54: E = (( dom fp) /\ ( dom (( - 1) (#) fm))) and

       A55: ( Integral (M,(fp + (( - 1) (#) fm)))) = (( Integral (M,(fp | E))) + ( Integral (M,((( - 1) (#) fm) | E)))) by A51, MESFUNC6: 101;

      

       A56: ( dom fp) = ( dom f) by RFUNCT_3:def 10;

      ( dom (( - 1) (#) fm)) = ( dom fm) by VALUED_1:def 5

      .= Omega by A52, FUNCT_2:def 1;

      

      then

       A57: E = (Omega /\ Omega) by A56, A54, FUNCT_2:def 1

      .= Omega;

      

       A58: ( Integral (M,(fp + (( - 1) (#) fm)))) = (( Integral (M,fp)) + ( Integral (M,(( - 1) (#) fm)))) by A55, A57

      .= (( Integral (M,fp)) + ( - ( Integral (M,fm)))) by A19, A11, MESFUNC6: 102;

      

       A59: ( dom Fm) = ( dom am) by A38, Lm9;

      

       A60: for n be Nat st n in ( dom Fm) holds for x be object st x in (Fm . n) holds (fm . x) = (am . n)

      proof

        let n be Nat such that

         A61: n in ( dom Fm);

        let x be object;

        assume x in (Fm . n);

        then x in {(( canFS Dm) . n)} by A39, A61;

        then x = (( canFS Dm) . n) by TARSKI:def 1;

        hence (fm . x) = (am . n) by A59, A61, FUNCT_1: 12;

      end;

      fp is_simple_func_in Sigma & fp is nonnegative by Th6, MESFUNC6: 61;

      then

       A62: ( Integral (M,fp)) = ( Sum xp) by A56, A3, A7, A29, A8, A9, Lm1;

      ( dom ( canFS D)) = ( Seg ( len F)) by A1, FINSEQ_1:def 3;

      then

       A63: ( len F) = ( len ( canFS D)) by FINSEQ_1:def 3;

      

       A64: ( len x) = L by A13, FINSEQ_1:def 3;

      

       A65: ( dom (xp1 - xm1)) = (( dom xp1) /\ ( dom xm1)) by VALUED_1: 12

      .= ( dom x1) by A28, A42, A13, A29, A43, FINSEQ_1:def 3;

      

       A66: ( len xp1) = L by A7, FINSEQ_1:def 3

      .= ( len xm1) by A41, FINSEQ_1:def 3;

      

       A67: for k be Nat st k in ( dom x1) holds ((xp1 - xm1) . k) = (x1 . k)

      proof

        let k be Nat;

        

         A68: f = (fp - fm) by MESFUNC6: 42;

        assume

         A69: k in ( dom x1);

        then

        reconsider z = (M . {(( canFS Omega) . k)}) as Element of REAL by A1, A17, A20, A15;

        

         A70: (xm1 . k) = ((fm . (( canFS Omega) . k)) * (M . {(( canFS Omega) . k)})) by A13, A41, A45, A69

        .= ((fm . (( canFS Omega) . k)) * z) by EXTREAL1: 1;

        k in ( dom ( canFS Omega)) by A1, A20, A69, FUNCT_2:def 1;

        then (( canFS Omega) . k) in ( rng ( canFS Omega)) by FUNCT_1: 3;

        then (( canFS Omega) . k) in Omega;

        then

         A71: (( canFS Omega) . k) in ( dom f) by FUNCT_2:def 1;

        k in (( dom xp1) /\ ( dom xm1)) by A13, A7, A41, A69;

        then

         A72: k in ( dom (xp1 - xm1)) by VALUED_1: 12;

        (xp1 . k) = ((fp . (( canFS Omega) . k)) * (M . {(( canFS Omega) . k)})) by A13, A7, A31, A69

        .= ((fp . (( canFS Omega) . k)) * z) by EXTREAL1: 1;

        

        hence ((xp1 - xm1) . k) = (((fp . (( canFS Omega) . k)) * z) - ((fm . (( canFS Omega) . k)) * z)) by A72, A70, VALUED_1: 13

        .= (((fp . (( canFS Omega) . k)) - (fm . (( canFS Omega) . k)) qua Real) * z)

        .= ((f . (( canFS Omega) . k)) * z) by A71, A68, VALUED_1: 13

        .= ((f . (( canFS Omega) . k)) * (M . {(( canFS Omega) . k)})) by EXTREAL1: 1

        .= (x1 . k) by A21, A69;

      end;

      ( Integral (M,f)) = ( Integral (M,(fp - fm))) by MESFUNC6: 42

      .= (( Sum xp) - ( Sum xm)) by A52, A37, A27, A41, A43, A62, A58, A59, A60, Lm1

      .= (( Sum xp1) - ( Sum xm1)) by A50, SUPINF_2: 3

      .= ( Sum (xp1 - xm1)) by A66, INTEGRA5: 2

      .= ( Sum x) by A65, A67, FINSEQ_1: 13, MESFUNC3: 2;

      hence thesis by A17, A21, A64, A63, FINSEQ_1: 93;

    end;

    theorem :: RANDOM_1:9

    

     Th9: for Omega be non empty finite set, M be sigma_Measure of ( Trivial-SigmaField Omega), f be Function of Omega, REAL , x be FinSequence of ExtREAL , s be FinSequence of Omega st s is one-to-one & ( rng s) = Omega holds ex F be Finite_Sep_Sequence of ( Trivial-SigmaField Omega), a be FinSequence of REAL st ( dom f) = ( union ( rng F)) & ( dom a) = ( dom s) & ( dom F) = ( dom s) & (for k be Nat st k in ( dom F) holds (F . k) = {(s . k)}) & for n be Nat holds for x,y be Element of Omega st n in ( dom F) & x in (F . n) & y in (F . n) holds (f . x) = (f . y)

    proof

      let Omega be non empty finite set, M be sigma_Measure of ( Trivial-SigmaField Omega), f be Function of Omega, REAL , x be FinSequence of ExtREAL , s be FinSequence of Omega;

      assume that

       A1: s is one-to-one and

       A2: ( rng s) = Omega;

      defpred Q[ Nat, set] means $2 = (f . (s . $1));

      set Sigma = ( Trivial-SigmaField Omega);

      set L = ( len s);

      defpred P[ Nat, set] means $2 = {(s . $1)};

      

       A3: for k be Nat st k in ( Seg L) holds ex x be Element of ( bool Omega) st P[k, x]

      proof

        let k be Nat;

        assume

         A4: k in ( Seg L);

        take {(s . k)};

        k in ( dom s) by A4, FINSEQ_1:def 3;

        then (s . k) in ( rng s) by FUNCT_1: 3;

        hence thesis by ZFMISC_1: 31;

      end;

      consider F be FinSequence of ( bool Omega) such that

       A5: ( dom F) = ( Seg L) & for k be Nat st k in ( Seg L) holds P[k, (F . k)] from FINSEQ_1:sch 5( A3);

       A6:

      now

        let i,j be Nat;

        assume that

         A7: i in ( dom F) & j in ( dom F) and

         A8: i <> j;

        i in ( dom s) & j in ( dom s) by A5, A7, FINSEQ_1:def 3;

        then

         A9: (s . i) <> (s . j) by A1, A8, FUNCT_1:def 4;

        (F . i) = {(s . i)} & (F . j) = {(s . j)} by A5, A7;

        hence (F . i) misses (F . j) by A9, ZFMISC_1: 11;

      end;

      

       A10: ( dom F) = ( dom s) by A5, FINSEQ_1:def 3;

      reconsider F as Finite_Sep_Sequence of Sigma by A6, MESFUNC3: 4;

      ( union ( rng F)) = ( rng s)

      proof

        now

          let x be object;

          assume x in ( union ( rng F));

          then

          consider y be set such that

           A11: x in y and

           A12: y in ( rng F) by TARSKI:def 4;

          consider n be object such that

           A13: n in ( dom F) and

           A14: y = (F . n) by A12, FUNCT_1:def 3;

          (F . n) = {(s . n)} by A5, A13;

          then

           A15: x = (s . n) by A11, A14, TARSKI:def 1;

          n in ( dom s) by A5, A13, FINSEQ_1:def 3;

          hence x in ( rng s) by A15, FUNCT_1:def 3;

        end;

        hence ( union ( rng F)) c= ( rng s);

        let x be object;

        assume x in ( rng s);

        then

        consider n be object such that

         A16: n in ( dom s) and

         A17: x = (s . n) by FUNCT_1:def 3;

        

         A18: n in ( Seg L) by A16, FINSEQ_1:def 3;

        reconsider n as Element of NAT by A16;

        n in ( dom F) by A5, A16, FINSEQ_1:def 3;

        then

         A19: (F . n) in ( rng F) by FUNCT_1:def 3;

        x in {(s . n)} by A17, TARSKI:def 1;

        then x in (F . n) by A5, A18;

        hence x in ( union ( rng F)) by A19, TARSKI:def 4;

      end;

      then

       A20: ( dom f) = ( union ( rng F)) by A2, FUNCT_2:def 1;

      take F;

      

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

      proof

        let n be Nat;

        let x,y be Element of Omega;

        assume that

         A22: n in ( dom F) and

         A23: x in (F . n) and

         A24: y in (F . n);

        

         A25: (F . n) = {(s . n)} by A5, A22;

        

        hence (f . x) = (f . (s . n)) by A23, TARSKI:def 1

        .= (f . y) by A24, A25, TARSKI:def 1;

      end;

      

       A26: for k be Nat st k in ( Seg L) holds ex x be Element of REAL st Q[k, x]

      proof

        let k be Nat;

        (f . (s . k)) in REAL by XREAL_0:def 1;

        hence thesis;

      end;

      ex a be FinSequence of REAL st (( dom a) = ( Seg L) & for k be Nat st k in ( Seg L) holds Q[k, (a . k)]) from FINSEQ_1:sch 5( A26);

      hence thesis by A5, A10, A20, A21;

    end;

    theorem :: RANDOM_1:10

    

     Th10: for Omega be non empty finite set, M be sigma_Measure of ( Trivial-SigmaField Omega), f be Function of Omega, REAL , x be FinSequence of ExtREAL , s be FinSequence of Omega st (M . Omega) < +infty & ( len x) = ( card Omega) & s is one-to-one & ( rng s) = Omega & ( len s) = ( card Omega) & (for n be Nat st n in ( dom x) holds (x . n) = ((f . (s . n)) qua ExtReal * (M . {(s . n)}))) holds ( Integral (M,f)) = ( Sum x)

    proof

      let Omega be non empty finite set, M be sigma_Measure of ( Trivial-SigmaField Omega), f be Function of Omega, REAL , x be FinSequence of ExtREAL , s be FinSequence of Omega;

      assume that

       A1: (M . Omega) < +infty and

       A2: ( len x) = ( card Omega) and

       A3: s is one-to-one and

       A4: ( rng s) = Omega and

       A5: ( len s) = ( card Omega) and

       A6: for n be Nat st n in ( dom x) holds (x . n) = ((f . (s . n)) qua ExtReal * (M . {(s . n)}));

      set Sigma = ( Trivial-SigmaField Omega);

      consider F be Finite_Sep_Sequence of Sigma, a be FinSequence of REAL such that

       A7: ( dom f) = ( union ( rng F)) and ( dom a) = ( dom s) and

       A8: ( dom F) = ( dom s) and

       A9: for k be Nat st k in ( dom F) holds (F . k) = {(s . k)} and for n be Nat holds for x,y be Element of Omega st n in ( dom F) & x in (F . n) & y in (F . n) holds (f . x) = (f . y) by A3, A4, Th9;

      

       A10: ( dom x) = ( Seg ( len s)) by A2, A5, FINSEQ_1:def 3

      .= ( dom F) by A8, FINSEQ_1:def 3;

      set fm = ( max- f);

      set fp = ( max+ f);

      

       A11: ( dom f) = Omega by FUNCT_2:def 1;

      then ( dom fp) = Omega by RFUNCT_3:def 10;

      then

       A12: fp is_integrable_on M by A1, Lm5, Th6;

      

       A13: for n be Nat st n in ( dom s) holds (M . {(s . n)}) in REAL

      proof

        let n be Nat;

        assume n in ( dom s);

        then (s . n) in ( rng s) by FUNCT_1: 3;

        then {(s . n)} c= Omega by ZFMISC_1: 31;

        hence (M . {(s . n)}) in REAL by A1, A4, Lm7;

      end;

      now

        let y be object;

        assume y in ( rng x);

        then

        consider n be Element of NAT such that

         A14: n in ( dom x) and

         A15: y = (x . n) by PARTFUN1: 3;

        reconsider z = (M . {(s . n)}) as Element of REAL by A8, A10, A13, A14;

        reconsider w = (f . (s . n)) as Element of REAL by XREAL_0:def 1;

        (x . n) = ((f . (s . n)) * (M . {(s . n)})) by A6, A14

        .= (w * z) by EXTREAL1: 1;

        hence y in REAL by A15;

      end;

      then ( rng x) c= REAL ;

      then

      reconsider x1 = x as FinSequence of REAL by FINSEQ_1:def 4;

      

       A16: fm is_simple_func_in Sigma & fm is nonnegative by Th6, MESFUNC6: 61;

      defpred AP[ Nat, set] means for x be object st x in (F . $1) holds $2 = (fp . x);

      set L = ( len F);

      

       A17: ( dom F) = ( Seg L) by FINSEQ_1:def 3;

      

       A18: for k be Nat st k in ( Seg L) holds ex y be Element of REAL st AP[k, y]

      proof

        let k be Nat;

        assume

         A19: k in ( Seg L);

        reconsider fpsk = (fp . (s . k)) as Element of REAL by XREAL_0:def 1;

        take fpsk;

        (F . k) = {(s . k)} by A9, A17, A19;

        hence thesis by TARSKI:def 1;

      end;

      consider ap be FinSequence of REAL such that

       A20: ( dom ap) = ( Seg L) & for k be Nat st k in ( Seg L) holds AP[k, (ap . k)] from FINSEQ_1:sch 5( A18);

      defpred AM[ Nat, set] means for x be object st x in (F . $1) holds $2 = (fm . x);

      

       A21: for k be Nat st k in ( Seg L) holds ex y be Element of REAL st AM[k, y]

      proof

        let k be Nat;

        assume

         A22: k in ( Seg L);

        reconsider fmsk = (fm . (s . k)) as Element of REAL by XREAL_0:def 1;

        take fmsk;

        (F . k) = {(s . k)} by A9, A17, A22;

        hence thesis by TARSKI:def 1;

      end;

      consider am be FinSequence of REAL such that

       A23: ( dom am) = ( Seg L) & for k be Nat st k in ( Seg L) holds AM[k, (am . k)] from FINSEQ_1:sch 5( A21);

      

       A24: ( dom fm) = ( dom f) by RFUNCT_3:def 11;

      then

       A25: fm is Function of Omega, REAL by A11, FUNCT_2:def 1;

      then (M . ( dom (( - 1) (#) fm))) < +infty by A1, FUNCT_2:def 1;

      then (( - 1) (#) fm) is_integrable_on M by A25, Lm5, Th6;

      then

      consider E be Element of Sigma such that

       A26: E = (( dom fp) /\ ( dom (( - 1) (#) fm))) and

       A27: ( Integral (M,(fp + (( - 1) (#) fm)))) = (( Integral (M,(fp | E))) + ( Integral (M,((( - 1) (#) fm) | E)))) by A12, MESFUNC6: 101;

      

       A28: (( - jj) * ( Integral (M,fm))) = (( - jj qua ExtReal) * ( Integral (M,fm)))

      .= ( - (1 qua ExtReal * ( Integral (M,fm)))) by XXREAL_3: 92

      .= ( - ( Integral (M,fm))) by XXREAL_3: 81;

      defpred Pp[ Nat, set] means $2 = ((ap . $1) * ((M * F) . $1));

      

       A29: for k be Nat st k in ( Seg L) holds ex x be Element of ExtREAL st Pp[k, x];

      consider xp be FinSequence of ExtREAL such that

       A30: ( dom xp) = ( Seg L) & for k be Nat st k in ( Seg L) holds Pp[k, (xp . k)] from FINSEQ_1:sch 5( A29);

      

       A31: ( dom xp) = ( dom F) by A30, FINSEQ_1:def 3;

      

       A32: for n be Nat st n in ( dom xp) holds (xp . n) = ((fp . (s . n)) * (M . {(s . n)}))

      proof

        let n be Nat;

        assume

         A33: n in ( dom xp);

        

        then

         A34: ((M * F) . n) = (M . (F . n)) by A31, FUNCT_1: 13

        .= (M . {(s . n)}) by A9, A31, A33;

        (F . n) = {(s . n)} by A9, A31, A33;

        then

         A35: (s . n) in (F . n) by TARSKI:def 1;

        

        thus (xp . n) = ((ap . n) * ((M * F) . n)) by A30, A33

        .= ((fp . (s . n)) * (M . {(s . n)})) by A20, A30, A33, A35, A34;

      end;

      now

        let y be object;

        assume y in ( rng xp);

        then

        consider n be Element of NAT such that

         A36: n in ( dom xp) and

         A37: y = (xp . n) by PARTFUN1: 3;

        reconsider z = (M . {(s . n)}) as Element of REAL by A8, A31, A13, A36;

        reconsider w = (fp . (s . n)) as Element of REAL by XREAL_0:def 1;

        (xp . n) = ((fp . (s . n)) * (M . {(s . n)})) by A32, A36

        .= (w * z) by EXTREAL1: 1;

        hence y in REAL by A37;

      end;

      then ( rng xp) c= REAL ;

      then

      reconsider xp1 = xp as FinSequence of REAL by FINSEQ_1:def 4;

      defpred Pm[ Nat, set] means $2 = ((am . $1) * ((M * F) . $1));

      

       A38: for k be Nat st k in ( Seg L) holds ex x be Element of ExtREAL st Pm[k, x];

      consider xm be FinSequence of ExtREAL such that

       A39: ( dom xm) = ( Seg L) & for k be Nat st k in ( Seg L) holds Pm[k, (xm . k)] from FINSEQ_1:sch 5( A38);

      

       A40: ( dom xm) = ( dom F) by A39, FINSEQ_1:def 3;

      

       A41: for n be Nat st n in ( dom xm) holds (xm . n) = ((fm . (s . n)) * (M . {(s . n)}))

      proof

        let n be Nat;

        assume

         A42: n in ( dom xm);

        

        then

         A43: ((M * F) . n) = (M . (F . n)) by A40, FUNCT_1: 13

        .= (M . {(s . n)}) by A9, A40, A42;

        (F . n) = {(s . n)} by A9, A40, A42;

        then

         A44: (s . n) in (F . n) by TARSKI:def 1;

        

        thus (xm . n) = ((am . n) * ((M * F) . n)) by A39, A42

        .= ((fm . (s . n)) * (M . {(s . n)})) by A23, A39, A42, A44, A43;

      end;

      now

        let y be object;

        assume y in ( rng xm);

        then

        consider n be Element of NAT such that

         A45: n in ( dom xm) and

         A46: y = (xm . n) by PARTFUN1: 3;

        reconsider z = (M . {(s . n)}) as Element of REAL by A8, A40, A13, A45;

        reconsider w = (fm . (s . n)) as Element of REAL by XREAL_0:def 1;

        (xm . n) = ((fm . (s . n)) * (M . {(s . n)})) by A41, A45

        .= (w * z) by EXTREAL1: 1;

        hence y in REAL by A46;

      end;

      then ( rng xm) c= REAL ;

      then

      reconsider xm1 = xm as FinSequence of REAL by FINSEQ_1:def 4;

      

       A47: ( Sum xp) = ( Sum xp1) & ( Sum xm) = ( Sum xm1) by MESFUNC3: 2;

      

       A48: for k be Nat st k in ( dom x1) holds ((xp1 - xm1) . k) = (x1 . k)

      proof

        let k be Nat;

        

         A49: f = (fp - fm) by MESFUNC6: 42;

        assume

         A50: k in ( dom x1);

        then

        reconsider z = (M . {(s . k)}) as Element of REAL by A8, A10, A13;

        

         A51: (xm1 . k) = ((fm . (s . k)) * (M . {(s . k)})) by A10, A40, A41, A50

        .= ((fm . (s . k)) * z) by EXTREAL1: 1;

        (s . k) in ( rng s) by A8, A10, A50, FUNCT_1: 3;

        then (s . k) in Omega;

        then

         A52: (s . k) in ( dom f) by FUNCT_2:def 1;

        k in (( dom xp1) /\ ( dom xm1)) by A10, A31, A40, A50;

        then

         A53: k in ( dom (xp1 - xm1)) by VALUED_1: 12;

        (xp1 . k) = ((fp . (s . k)) * (M . {(s . k)})) by A10, A31, A32, A50

        .= ((fp . (s . k)) * z) by EXTREAL1: 1;

        

        hence ((xp1 - xm1) . k) = (((fp . (s . k)) * z) - ((fm . (s . k)) * z)) by A53, A51, VALUED_1: 13

        .= (((fp . (s . k)) - (fm . (s . k)) qua Real) * z)

        .= ((f . (s . k)) * z) by A52, A49, VALUED_1: 13

        .= ((f . (s . k)) * (M . {(s . k)})) by EXTREAL1: 1

        .= (x1 . k) by A6, A50;

      end;

      ( dom fm) = Omega by A11, RFUNCT_3:def 11;

      then

       A54: fm is_integrable_on M by A1, Lm5, Th6;

      

       A55: ( dom fp) = ( dom f) by RFUNCT_3:def 10;

      

       A56: ( dom (xp1 - xm1)) = (( dom xp1) /\ ( dom xm1)) by VALUED_1: 12

      .= ( dom x1) by A10, A31, A40;

      

       A57: ( len xp1) = L by A30, FINSEQ_1:def 3

      .= ( len xm1) by A39, FINSEQ_1:def 3;

      ( dom (( - 1) (#) fm)) = ( dom fm) by VALUED_1:def 5

      .= Omega by A11, RFUNCT_3:def 11;

      

      then

       A58: E = (Omega /\ Omega) by A11, A26, RFUNCT_3:def 10

      .= Omega;

      

       A59: ( Integral (M,(fp + (( - 1) (#) fm)))) = (( Integral (M,fp)) + ( Integral (M,(( - 1) (#) fm)))) by A27, A58

      .= (( Integral (M,fp)) + ( - ( Integral (M,fm)))) by A54, A28, MESFUNC6: 102;

      fp is_simple_func_in Sigma & fp is nonnegative by Th6, MESFUNC6: 61;

      then

       A60: ( Integral (M,fp)) = ( Sum xp) by A7, A55, A17, A20, A30, Lm1;

      

      thus ( Integral (M,f)) = ( Integral (M,(fp - fm))) by MESFUNC6: 42

      .= (( Sum xp) - ( Sum xm)) by A7, A24, A17, A23, A16, A39, A60, A59, Lm1

      .= (( Sum xp1) - ( Sum xm1)) by A47, SUPINF_2: 3

      .= ( Sum (xp1 - xm1)) by A57, INTEGRA5: 2

      .= ( Sum x) by A56, A48, FINSEQ_1: 13, MESFUNC3: 2;

    end;

    theorem :: RANDOM_1:11

    for Omega be non empty finite set, M be sigma_Measure of ( Trivial-SigmaField Omega), f be Function of Omega, REAL st (M . Omega) < +infty holds ex x be FinSequence of ExtREAL , s be FinSequence of Omega st ( len x) = ( card Omega) & s is one-to-one & ( rng s) = Omega & ( len s) = ( card Omega) & (for n be Nat st n in ( dom x) holds (x . n) = ((f . (s . n)) qua ExtReal * (M . {(s . n)}))) & ( Integral (M,f)) = ( Sum x)

    proof

      let Omega be non empty finite set, M be sigma_Measure of ( Trivial-SigmaField Omega), f be Function of Omega, REAL ;

      set s = ( canFS Omega);

      assume (M . Omega) < +infty ;

      then

       A1: ex x be FinSequence of ExtREAL st ( len x) = ( card Omega) & (for n be Nat st n in ( dom x) holds (x . n) = ((f . (( canFS Omega) . n)) qua ExtReal * (M . {(( canFS Omega) . n)}))) & ( Integral (M,f)) = ( Sum x) by Lm10;

      ( rng s) = Omega & ( len s) = ( card Omega) by FINSEQ_1: 93, FUNCT_2:def 3;

      hence thesis by A1;

    end;

    

     Lm11: for Omega be non empty finite set, P be Probability of ( Trivial-SigmaField Omega), f be Function of Omega, REAL holds ex F be FinSequence of REAL st ( len F) = ( card Omega) & (for n be Nat st n in ( dom F) holds (F . n) = ((f . (( canFS Omega) . n)) * (P . {(( canFS Omega) . n)}))) & ( Integral (( P2M P),f)) = ( Sum F)

    proof

      let Omega be non empty finite set, P be Probability of ( Trivial-SigmaField Omega), f be Function of Omega, REAL ;

      set Sigma = ( Trivial-SigmaField Omega);

      set M = ( P2M P);

      

       A1: (P . Omega) in REAL by XREAL_0:def 1;

      then

      consider x be FinSequence of ExtREAL such that

       A2: ( len x) = ( card Omega) and

       A3: for n be Nat st n in ( dom x) holds (x . n) = ((f . (( canFS Omega) . n)) qua ExtReal * (( P2M P) . {(( canFS Omega) . n)})) and

       A4: ( Integral (( P2M P),f)) = ( Sum x) by Lm10, XXREAL_0: 9;

      

       A5: (( P2M P) . Omega) < +infty by A1, XXREAL_0: 9;

      

       A6: for n be Nat st n in ( dom ( canFS Omega)) holds (M . {(( canFS Omega) . n)}) in REAL

      proof

        let n be Nat;

        assume n in ( dom ( canFS Omega));

        then (( canFS Omega) . n) in ( rng ( canFS Omega)) by FUNCT_1: 3;

        then

         A7: {(( canFS Omega) . n)} c= Omega by ZFMISC_1: 31;

        Omega in Sigma by MEASURE1: 7;

        hence (M . {(( canFS Omega) . n)}) in REAL by A5, A7, Lm7;

      end;

      now

        let y be object;

        assume y in ( rng x);

        then

        consider n be Element of NAT such that

         A8: n in ( dom x) and

         A9: y = (x . n) by PARTFUN1: 3;

        ( Seg ( len x)) = ( Seg ( len ( canFS Omega))) by A2, FINSEQ_1: 93;

        then ( dom x) = ( Seg ( len ( canFS Omega))) by FINSEQ_1:def 3;

        then n in ( dom ( canFS Omega)) by A8, FINSEQ_1:def 3;

        then

        reconsider z = (M . {(( canFS Omega) . n)}) as Element of REAL by A6;

        reconsider w = (f . (( canFS Omega) . n)) as Element of REAL by XREAL_0:def 1;

        (x . n) = ((f . (( canFS Omega) . n)) * (M . {(( canFS Omega) . n)})) by A3, A8

        .= (w * z) by EXTREAL1: 1;

        hence y in REAL by A9;

      end;

      then ( rng x) c= REAL ;

      then

      reconsider F = x as FinSequence of REAL by FINSEQ_1:def 4;

      take F;

      for n be Nat st n in ( dom F) holds (F . n) = ((f . (( canFS Omega) . n)) * (P . {(( canFS Omega) . n)})) by A3;

      hence thesis by A2, A4, MESFUNC3: 2;

    end;

    theorem :: RANDOM_1:12

    

     Th12: for Omega be non empty finite set, P be Probability of ( Trivial-SigmaField Omega), f be Function of Omega, REAL , x be FinSequence of REAL , s be FinSequence of Omega st ( len x) = ( card Omega) & s is one-to-one & ( rng s) = Omega & ( len s) = ( card Omega) & (for n be Nat st n in ( dom x) holds (x . n) = ((f . (s . n)) * (P . {(s . n)}))) holds ( Integral (( P2M P),f)) = ( Sum x)

    proof

      let Omega be non empty finite set, P be Probability of ( Trivial-SigmaField Omega), f be Function of Omega, REAL , x be FinSequence of REAL , s be FinSequence of Omega;

      assume that

       A1: ( len x) = ( card Omega) & s is one-to-one & ( rng s) = Omega & ( len s) = ( card Omega) and

       A2: for n be Nat st n in ( dom x) holds (x . n) = ((f . (s . n)) * (P . {(s . n)}));

      set M = ( P2M P);

      ( rng x) c= ExtREAL by NUMBERS: 31;

      then

      reconsider x1 = x as FinSequence of ExtREAL by FINSEQ_1:def 4;

      

       A3: for n be Nat st n in ( dom x1) holds (x1 . n) = ((f . (s . n)) * (( P2M P) . {(s . n)})) by A2;

      (P . Omega) in REAL by XREAL_0:def 1;

      

      then ( Integral (M,f)) = ( Sum x1) by A1, A3, Th10, XXREAL_0: 9

      .= ( Sum x) by MESFUNC3: 2;

      hence thesis;

    end;

    theorem :: RANDOM_1:13

    

     Th13: for Omega be non empty finite set, P be Probability of ( Trivial-SigmaField Omega), f be Function of Omega, REAL holds ex F be FinSequence of REAL , s be FinSequence of Omega st ( len F) = ( card Omega) & s is one-to-one & ( rng s) = Omega & ( len s) = ( card Omega) & (for n be Nat st n in ( dom F) holds (F . n) = ((f . (s . n)) * (P . {(s . n)}))) & ( Integral (( P2M P),f)) = ( Sum F)

    proof

      let Omega be non empty finite set, P be Probability of ( Trivial-SigmaField Omega), f be Function of Omega, REAL ;

      set s = ( canFS Omega);

      

       A1: ( len s) = ( card Omega) by FINSEQ_1: 93;

      (ex F be FinSequence of REAL st ( len F) = ( card Omega) & (for n be Nat st n in ( dom F) holds (F . n) = ((f . (( canFS Omega) . n)) * (P . {(( canFS Omega) . n)}))) & ( Integral (( P2M P),f)) = ( Sum F)) & ( rng s) = Omega by Lm11, FUNCT_2:def 3;

      hence thesis by A1;

    end;

    theorem :: RANDOM_1:14

    

     Th14: for E be finite non empty set, ASeq be SetSequence of E st ASeq is non-ascending holds ex N be Nat st for m be Nat st N <= m holds (ASeq . N) = (ASeq . m)

    proof

      let E be finite non empty set, ASeq be SetSequence of E;

      defpred P[ Element of NAT , set] means $2 = ( card (ASeq . $1));

      

       A1: for x be Element of NAT holds ex y be Element of REAL st P[x, y]

      proof

        let x be Element of NAT ;

        ( card (ASeq . x)) in REAL by NUMBERS: 19;

        hence thesis;

      end;

      consider seq be sequence of REAL such that

       A2: for n be Element of NAT holds P[n, (seq . n)] from FUNCT_2:sch 3( A1);

      now

        let m be Nat;

        reconsider mm = m as Element of NAT by ORDINAL1:def 12;

        (seq . mm) = ( card (ASeq . mm)) by A2;

        hence ( - 1) < (seq . m);

      end;

      then

       A3: seq is bounded_below by SEQ_2:def 4;

      assume

       A4: ASeq is non-ascending;

       A5:

      now

        let n,m be Nat;

        assume n <= m;

        then

         A6: (ASeq . m) c= (ASeq . n) by A4, PROB_1:def 4;

        reconsider mm = m, nn = n as Element of NAT by ORDINAL1:def 12;

        (seq . mm) = ( card (ASeq . mm)) & (seq . nn) = ( card (ASeq . nn)) by A2;

        hence (seq . m) <= (seq . n) by A6, NAT_1: 43;

      end;

      then seq is non-increasing by SEQM_3: 8;

      then

      consider g be Real such that

       A7: for p be Real st 0 < p holds ex n be Nat st for m be Nat st n <= m holds |.((seq . m) - g) qua Complex.| < p by A3, SEQ_2:def 6;

      consider N be Nat such that

       A8: for m be Nat st N <= m holds |.((seq . m) - g) qua Complex.| < (1 / 2) by A7;

      reconsider NN = N as Element of NAT by ORDINAL1:def 12;

      take N;

      now

         |.((seq . N) - g) qua Complex.| < (1 / 2) by A8;

        then

         A9: |.(g - (seq . N)) qua Complex.| < (1 / 2) by COMPLEX1: 60;

        let m be Nat;

        reconsider mm = m as Element of NAT by ORDINAL1:def 12;

        

         A10: (seq . NN) = ( card (ASeq . NN)) & (seq . mm) = ( card (ASeq . mm)) by A2;

        assume

         A11: N <= m;

        then

         A12: (seq . m) <= (seq . N) & (ASeq . m) c= (ASeq . N) by A4, A5, PROB_1:def 4;

         |.((seq . m) - g) qua Complex.| < (1 / 2) by A8, A11;

        then

         A13: ( |.((seq . m) - g) qua Complex.| + |.(g - (seq . N)) qua Complex.|) < ((1 / 2) + (1 / 2)) by A9, XREAL_1: 8;

         |.((seq . m) - (seq . N) qua Real) qua Complex.| <= ( |.((seq . m) - g) qua Complex.| + |.(g - (seq . N)) qua Complex.|) by COMPLEX1: 63;

        then |.((seq . m) - (seq . N) qua Real) qua Complex.| < 1 by A13, XXREAL_0: 2;

        then |.((seq . N) qua Real - (seq . m)) qua Complex.| < 1 by COMPLEX1: 60;

        then ((seq . N) qua Real - (seq . m)) < 1 by ABSVALUE:def 1;

        then (((seq . N) qua Real - (seq . m)) + (seq . m)) < (1 + (seq . m)) by XREAL_1: 8;

        then (seq . NN) qua Real <= (seq . m) by A10, NAT_1: 8;

        hence (ASeq . m) = (ASeq . N) by A10, A12, CARD_2: 102, XXREAL_0: 1;

      end;

      hence thesis;

    end;

    theorem :: RANDOM_1:15

    

     Th15: for E be finite non empty set, ASeq be SetSequence of E st ASeq is non-ascending holds ex N be Nat st for m be Nat st N <= m holds ( Intersection ASeq) = (ASeq . m)

    proof

      let E be finite non empty set, ASeq be SetSequence of E;

      assume

       A1: ASeq is non-ascending;

      then

      consider N0 be Nat such that

       A2: for m be Nat st N0 <= m holds (ASeq . N0) = (ASeq . m) by Th14;

      take N0;

      let N be Nat;

      assume N0 <= N;

      then

       A3: (ASeq . N) = (ASeq . N0) by A2;

      thus ( Intersection ASeq) = (ASeq . N)

      proof

        for x be object st x in ( Intersection ASeq) holds x in (ASeq . N) by PROB_1: 13;

        hence ( Intersection ASeq) c= (ASeq . N);

        let x be object;

        assume

         A4: x in (ASeq . N);

        now

          let n be Nat;

          per cases ;

            suppose n <= N0;

            then (ASeq . N0) c= (ASeq . n) by A1, PROB_1:def 4;

            hence x in (ASeq . n) by A3, A4;

          end;

            suppose N0 < n;

            hence x in (ASeq . n) by A2, A3, A4;

          end;

        end;

        hence x in ( Intersection ASeq) by PROB_1: 13;

      end;

    end;

    theorem :: RANDOM_1:16

    

     Th16: for E be finite non empty set, ASeq be SetSequence of E st ASeq is non-descending holds ex N be Nat st for m be Nat st N <= m holds (ASeq . N) = (ASeq . m)

    proof

      let E be finite non empty set, ASeq be SetSequence of E;

      defpred P[ Element of NAT , set] means $2 = ( card (ASeq . $1));

      

       A1: for x be Element of NAT holds ex y be Element of REAL st P[x, y]

      proof

        let x be Element of NAT ;

        ( card (ASeq . x)) in REAL by NUMBERS: 19;

        hence thesis;

      end;

      consider seq be sequence of REAL such that

       A2: for n be Element of NAT holds P[n, (seq . n)] from FUNCT_2:sch 3( A1);

      now

        let n be Nat;

        reconsider nn = n as Element of NAT by ORDINAL1:def 12;

        ( card (ASeq . nn)) <= ( card E) by NAT_1: 43;

        then ( card (ASeq . nn)) < (( card E) + 1) by NAT_1: 13;

        hence (seq . n) < (( card E) + 1) by A2;

      end;

      then

       A3: seq is bounded_above by SEQ_2:def 3;

      assume

       A4: ASeq is non-descending;

       A5:

      now

        let n,m be Nat;

        reconsider mm = m, nn = n as Element of NAT by ORDINAL1:def 12;

        assume n <= m;

        then

         A6: (ASeq . n) c= (ASeq . m) by A4, PROB_1:def 5;

        (seq . mm) = ( card (ASeq . mm)) & (seq . nn) = ( card (ASeq . nn)) by A2;

        hence (seq . n) <= (seq . m) by A6, NAT_1: 43;

      end;

      then seq is non-decreasing by SEQM_3: 6;

      then

      consider g be Real such that

       A7: for p be Real st 0 < p holds ex n be Nat st for m be Nat st n <= m holds |.((seq . m) - g) qua Complex.| < p by A3, SEQ_2:def 6;

      consider N be Nat such that

       A8: for m be Nat st N <= m holds |.((seq . m) - g) qua Complex.| < (1 / 2) by A7;

      take N;

      now

         |.((seq . N) - g) qua Complex.| < (1 / 2) by A8;

        then

         A9: |.(g - (seq . N)) qua Complex.| < (1 / 2) by COMPLEX1: 60;

        let m be Nat;

        reconsider NN = N, mm = m as Element of NAT by ORDINAL1:def 12;

        

         A10: (seq . NN) = ( card (ASeq . NN)) & (seq . mm) = ( card (ASeq . mm)) by A2;

        assume

         A11: N <= m;

        then

         A12: (seq . N) <= (seq . m) & (ASeq . N) c= (ASeq . m) by A4, A5, PROB_1:def 5;

         |.((seq . m) - g) qua Complex.| < (1 / 2) by A8, A11;

        then

         A13: ( |.((seq . m) - g) qua Complex.| + |.(g - (seq . N)) qua Complex.|) < ((1 / 2) + (1 / 2)) by A9, XREAL_1: 8;

         |.((seq . m) - (seq . N) qua Real) qua Complex.| <= ( |.((seq . m) - g) qua Complex.| + |.(g - (seq . N)) qua Complex.|) by COMPLEX1: 63;

        then |.((seq . m) - (seq . N) qua Real) qua Complex.| < 1 by A13, XXREAL_0: 2;

        then ((seq . m) - (seq . N) qua Real) < 1 by ABSVALUE:def 1;

        then (((seq . m) - (seq . N) qua Real) + (seq . N) qua Real) < (1 + (seq . N)) by XREAL_1: 8;

        then (seq . m) <= (seq . N) qua Real by A10, NAT_1: 8;

        hence (ASeq . m) = (ASeq . N) by A10, A12, CARD_2: 102, XXREAL_0: 1;

      end;

      hence thesis;

    end;

    theorem :: RANDOM_1:17

    for E be finite non empty set, ASeq be SetSequence of E st ASeq is non-descending holds ex N be Nat st for m be Nat st N <= m holds ( Union ASeq) = (ASeq . m)

    proof

      let E be finite non empty set, ASeq be SetSequence of E;

      assume

       A1: ASeq is non-descending;

      then

      consider N0 be Nat such that

       A2: for m be Nat st N0 <= m holds (ASeq . N0) = (ASeq . m) by Th16;

      reconsider N = N0 as Nat;

      take N;

      let m be Nat;

      reconsider M = m as Element of NAT by ORDINAL1:def 12;

      assume

       A3: N <= m;

      now

        let x be object;

        assume x in ( Union ASeq);

        then

        consider n be Nat such that

         A4: x in (ASeq . n) by PROB_1: 12;

        per cases ;

          suppose

           A5: n < N;

          

           A6: (ASeq . N) c= (ASeq . M) by A2, A3;

          (ASeq . n) c= (ASeq . N) by A1, A5, PROB_1:def 5;

          then (ASeq . n) c= (ASeq . m) by A6;

          hence x in (ASeq . m) by A4;

        end;

          suppose N <= n;

          then (ASeq . N) = (ASeq . n) by A2;

          then (ASeq . n) c= (ASeq . M) by A2, A3;

          hence x in (ASeq . m) by A4;

        end;

      end;

      then

       A7: ( Union ASeq) c= (ASeq . m);

      (ASeq . m) c= ( Union ASeq) by ABCMIZ_1: 1;

      hence (ASeq . m) = ( Union ASeq) by A7;

    end;

    definition

      let E;

      :: RANDOM_1:def1

      func Trivial-Probability (E) -> Probability of ( Trivial-SigmaField E) means

      : Def1: for A be Event of E holds (it . A) = ( prob A);

      existence

      proof

        deffunc F( Element of ( bool E)) = ( In (( prob $1), REAL ));

        consider EP be Function of ( Trivial-SigmaField E), REAL such that

         A1: for x be Element of ( Trivial-SigmaField E) holds (EP . x) = F(x) from FUNCT_2:sch 4;

        

         A2: for A,B be Event of ( Trivial-SigmaField E) st A misses B holds (EP . (A \/ B)) = ((EP . A) + (EP . B))

        proof

          let A,B be Event of ( Trivial-SigmaField E);

          assume

           A3: A misses B;

          

           A4: (EP . B) = F(B) by A1

          .= ( prob B);

          

          thus (EP . (A \/ B)) = F(\/) by A1

          .= ( prob (A \/ B))

          .= ((( prob A) + ( prob B)) - ( prob (A /\ B))) by RPR_1: 20

          .= ((( prob A) + ( prob B)) - 0 ) by A3, RPR_1: 16

          .= ( F(A) + ( prob B))

          .= ((EP . A) + ( prob B)) by A1

          .= ((EP . A) + (EP . B) qua Real) by A4

          .= ((EP . A) + (EP . B));

        end;

        

         A5: for A be Event of ( Trivial-SigmaField E) holds 0 <= (EP . A)

        proof

          let A be Event of ( Trivial-SigmaField E);

          (EP . A) = F(A) by A1

          .= ( prob A);

          hence thesis;

        end;

        

         A6: for ASeq be SetSequence of ( Trivial-SigmaField E) st ASeq is non-ascending holds (EP * ASeq) is convergent & ( lim (EP * ASeq)) = (EP . ( Intersection ASeq))

        proof

          let ASeq be SetSequence of ( Trivial-SigmaField E);

          assume ASeq is non-ascending;

          then

          consider N be Nat such that

           A7: for m be Nat st N <= m holds ( Intersection ASeq) = (ASeq . m) by Th15;

          now

            let m be Nat;

            assume

             A8: N <= m;

            m in NAT by ORDINAL1:def 12;

            then m in ( dom ASeq) by FUNCT_2:def 1;

            

            hence ((EP * ASeq) . m) = (EP . (ASeq . m)) by FUNCT_1: 13

            .= (EP . ( Intersection ASeq)) by A7, A8;

          end;

          hence thesis by PROB_1: 1;

        end;

        (EP . E) = F([#]) by A1

        .= ( prob ( [#] E))

        .= 1 by RPR_1: 15;

        then

        reconsider EP as Probability of ( Trivial-SigmaField E) by A5, A2, A6, PROB_1:def 8;

        take EP;

        let A be Event of E;

        

        thus (EP . A) = F(A) by A1

        .= ( prob A);

      end;

      uniqueness

      proof

        let F,G be Probability of ( Trivial-SigmaField E);

        assume

         A9: for A be Event of E holds (F . A) = ( prob A);

        assume

         A10: for A be Event of E holds (G . A) = ( prob A);

        now

          let x be object;

          assume x in ( Trivial-SigmaField E);

          then

          reconsider A = x as Event of E;

          

          thus (F . x) = ( prob A) by A9

          .= (G . x) by A10;

        end;

        hence thesis by FUNCT_2: 12;

      end;

    end

    definition

      let Omega, Sigma;

      :: RANDOM_1:def2

      mode Real-Valued-Random-Variable of Sigma -> Function of Omega, REAL means

      : Def2: it is ( [#] Sigma) -measurable;

      correctness

      proof

        reconsider X = ( [#] Sigma) as Element of Sigma;

        ( chi (X,Omega)) is real-valued by MESFUNC2: 28;

        then ( dom ( chi (X,Omega))) = Omega & ( rng ( chi (X,Omega))) c= REAL by FUNCT_3:def 3, VALUED_0:def 3;

        then

        reconsider f = ( chi (X,Omega)) as Function of Omega, REAL by FUNCT_2: 2;

        ( R_EAL f) = ( chi (X,Omega)) & ( chi (X,Omega)) is X -measurable by MESFUNC2: 29;

        then f is X -measurable;

        hence thesis;

      end;

    end

    reserve f,g for Real-Valued-Random-Variable of Sigma;

    theorem :: RANDOM_1:18

    

     Th18: (f + g) is Real-Valued-Random-Variable of Sigma

    proof

      f is ( [#] Sigma) -measurable & g is ( [#] Sigma) -measurable by Def2;

      then (f + g) is ( [#] Sigma) -measurable by MESFUNC6: 26;

      hence thesis by Def2;

    end;

    definition

      let Omega, Sigma, f, g;

      :: original: +

      redefine

      func f + g -> Real-Valued-Random-Variable of Sigma ;

      correctness by Th18;

    end

    theorem :: RANDOM_1:19

    

     Th19: (f - g) is Real-Valued-Random-Variable of Sigma

    proof

      

       A1: f is ( [#] Sigma) -measurable by Def2;

      set Y = ( [#] Sigma);

      

       A3: g is Y -measurable by Def2;

      ( dom g) = Y by FUNCT_2:def 1;

      then (f - g) is ( [#] Sigma) -measurable by MESFUNC6: 29, A1, A3;

      hence thesis by Def2;

    end;

    definition

      let Omega, Sigma, f, g;

      :: original: -

      redefine

      func f - g -> Real-Valued-Random-Variable of Sigma ;

      correctness by Th19;

    end

    theorem :: RANDOM_1:20

    

     Th20: for r be Real holds (r (#) f) is Real-Valued-Random-Variable of Sigma

    proof

      let r be Real;

      set X = ( [#] Sigma);

      

       A2: f is X -measurable by Def2;

      ( dom f) = X by FUNCT_2:def 1;

      then (r (#) f) is X -measurable by A2, MESFUNC6: 21;

      hence thesis by Def2;

    end;

    definition

      let Omega, Sigma, f;

      let r be Real;

      :: original: (#)

      redefine

      func r (#) f -> Real-Valued-Random-Variable of Sigma ;

      correctness by Th20;

    end

    theorem :: RANDOM_1:21

    

     Th21: for f,g be PartFunc of Omega, REAL holds (( R_EAL f) (#) ( R_EAL g)) = ( R_EAL (f (#) g))

    proof

      let f,g be PartFunc of Omega, REAL ;

      

       A1: ( dom (( R_EAL f) (#) ( R_EAL g))) = (( dom ( R_EAL f)) /\ ( dom ( R_EAL g))) by MESFUNC1:def 5

      .= ( dom (f (#) g)) by VALUED_1:def 4;

      now

        let x be object;

        assume

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

        

        hence ((( R_EAL f) (#) ( R_EAL g)) . x) = ((( R_EAL f) . x) * (( R_EAL g) . x)) by MESFUNC1:def 5

        .= ((f . x) * (g . x) qua Real) by EXTREAL1: 1

        .= ((f (#) g) . x) by A1, A2, VALUED_1:def 4;

      end;

      hence thesis by A1, FUNCT_1: 2;

    end;

    theorem :: RANDOM_1:22

    

     Th22: (f (#) g) is Real-Valued-Random-Variable of Sigma

    proof

      set X = ( [#] Sigma);

      

       A2: f is X -measurable by Def2;

      

       A3: ( R_EAL f) is X -measurable by A2;

      ( dom ( R_EAL f)) = X & ( dom ( R_EAL g)) = X by FUNCT_2:def 1;

      then

       A4: (( dom ( R_EAL f)) /\ ( dom ( R_EAL g))) = X;

      g is ( [#] Sigma) -measurable by Def2;

      then ( R_EAL g) is X -measurable;

      then (( R_EAL f) (#) ( R_EAL g)) is X -measurable by A3, A4, MESFUNC7: 15;

      then ( R_EAL (f (#) g)) is X -measurable by Th21;

      then (f (#) g) is X -measurable;

      hence thesis by Def2;

    end;

    definition

      let Omega, Sigma, f, g;

      :: original: (#)

      redefine

      func f (#) g -> Real-Valued-Random-Variable of Sigma ;

      correctness by Th22;

    end

    theorem :: RANDOM_1:23

    

     Th23: for r be Real st 0 <= r & f is nonnegative holds (f to_power r) is Real-Valued-Random-Variable of Sigma

    proof

      let r be Real;

      assume

       A1: 0 <= r & f is nonnegative;

      

       A2: ( dom f) = Omega by FUNCT_2:def 1;

      ( rng (f to_power r)) c= REAL & ( dom (f to_power r)) = ( dom f) by MESFUN6C:def 4;

      then

       A3: (f to_power r) is Function of Omega, REAL by A2, FUNCT_2: 2;

      

       A5: f is ( [#] Sigma) -measurable by Def2;

      ( dom f) = ( [#] Sigma) by FUNCT_2:def 1;

      then (f to_power r) is ( [#] Sigma) -measurable by A1, A5, MESFUN6C: 29;

      hence thesis by A3, Def2;

    end;

    

     Lm12: for X be non empty set, f be PartFunc of X, REAL holds ( abs f) is nonnegative

    proof

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

      now

        let x be object;

        assume x in ( dom ( abs f));

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

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

      end;

      hence ( abs f) is nonnegative by MESFUNC6: 52;

    end;

    theorem :: RANDOM_1:24

    

     Th24: ( abs f) is Real-Valued-Random-Variable of Sigma

    proof

      

       A2: f is ( [#] Sigma) -measurable by Def2;

      ( dom f) = ( [#] Sigma) & ( R_EAL f) is ( [#] Sigma) -measurable by A2, FUNCT_2:def 1;

      then |.( R_EAL f).| is ( [#] Sigma) -measurable by MESFUNC2: 27;

      then ( R_EAL ( abs f)) is ( [#] Sigma) -measurable by MESFUNC6: 1;

      then ( abs f) is ( [#] Sigma) -measurable;

      hence thesis by Def2;

    end;

    definition

      let Omega, Sigma, f;

      :: original: abs

      redefine

      func abs f -> Real-Valued-Random-Variable of Sigma ;

      correctness by Th24;

    end

    theorem :: RANDOM_1:25

    for r be Real st 0 <= r holds (( abs f) to_power r) is Real-Valued-Random-Variable of Sigma

    proof

      let r be Real;

      assume

       A1: 0 <= r;

      ( abs f) is nonnegative by Lm12;

      hence thesis by A1, Th23;

    end;

    definition

      let Omega, Sigma, f, P;

      :: RANDOM_1:def3

      pred f is_integrable_on P means f is_integrable_on ( P2M P);

    end

    definition

      let Omega, Sigma, P;

      let f be Real-Valued-Random-Variable of Sigma;

      assume

       A1: f is_integrable_on P;

      :: RANDOM_1:def4

      func expect (f,P) -> Real equals

      : Def4: ( Integral (( P2M P),f));

      correctness

      proof

        f is_integrable_on ( P2M P) by A1;

        then -infty < ( Integral (( P2M P),f)) & ( Integral (( P2M P),f)) < +infty by MESFUNC6: 90;

        then ( Integral (( P2M P),f)) in REAL by XXREAL_0: 48;

        hence thesis;

      end;

    end

    theorem :: RANDOM_1:26

    

     Th26: f is_integrable_on P & g is_integrable_on P implies ( expect ((f + g),P)) = (( expect (f,P)) + ( expect (g,P)))

    proof

      set h = (f + g);

      assume

       A1: f is_integrable_on P & g is_integrable_on P;

      then

       A2: ( Integral (( P2M P),f)) = ( expect (f,P)) & ( Integral (( P2M P),g)) = ( expect (g,P)) by Def4;

      

       A3: f is_integrable_on ( P2M P) & g is_integrable_on ( P2M P) by A1;

      then

      consider E be Element of Sigma such that

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

       A5: ( Integral (( P2M P),(f + g))) = (( Integral (( P2M P),(f | E))) + ( Integral (( P2M P),(g | E)))) by MESFUNC6: 101;

      

       A6: ( dom f) = Omega & ( dom g) = Omega by FUNCT_2:def 1;

      h is_integrable_on ( P2M P) by A3, MESFUNC6: 100;

      then h is_integrable_on P;

      

      hence ( expect (h,P)) = ( Integral (( P2M P),(f + g))) by Def4

      .= (( Integral (( P2M P),f)) + ( Integral (( P2M P),g))) by A4, A5, A6

      .= (( expect (f,P)) + ( expect (g,P))) by A2, SUPINF_2: 1;

    end;

    theorem :: RANDOM_1:27

    

     Th27: for r be Real holds f is_integrable_on P implies ( expect ((r (#) f),P)) = (r * ( expect (f,P)))

    proof

      let r be Real;

      set h = (r (#) f);

      assume

       A1: f is_integrable_on P;

      then

       A2: ( Integral (( P2M P),f)) = ( expect (f,P)) by Def4;

      

       A3: f is_integrable_on ( P2M P) by A1;

      then h is_integrable_on ( P2M P) by MESFUNC6: 102;

      then h is_integrable_on P;

      

      hence ( expect (h,P)) = ( Integral (( P2M P),(r (#) f))) by Def4

      .= (r * ( Integral (( P2M P),f))) by A3, MESFUNC6: 102

      .= (r * ( expect (f,P))) by A2, EXTREAL1: 1;

    end;

    theorem :: RANDOM_1:28

    f is_integrable_on P & g is_integrable_on P implies ( expect ((f - g),P)) = (( expect (f,P)) - ( expect (g,P)))

    proof

      assume that

       A1: f is_integrable_on P and

       A2: g is_integrable_on P;

      g is_integrable_on ( P2M P) by A2;

      then (( - 1) (#) g) is_integrable_on ( P2M P) by MESFUNC6: 102;

      then (( - jj) (#) g) is_integrable_on P;

      

      hence ( expect ((f - g),P)) = (( expect (f,P)) + ( expect ((( - jj) (#) g),P))) by A1, Th26

      .= (( expect (f,P)) + (( - 1) * ( expect (g,P)))) by A2, Th27

      .= (( expect (f,P)) - ( expect (g,P)));

    end;

    theorem :: RANDOM_1:29

    for Omega be non empty finite set, f be Function of Omega, REAL holds f is Real-Valued-Random-Variable of ( Trivial-SigmaField Omega)

    proof

      let Omega be non empty finite set, f be Function of Omega, REAL ;

      set Sigma = ( Trivial-SigmaField Omega);

      consider X be Element of ( Trivial-SigmaField Omega) such that

       A1: ( dom f) = X & f is X -measurable by Th8;

      

       A2: f is X -measurable & ( dom f) = Omega by FUNCT_2:def 1, A1;

      X = ( [#] Sigma) by A1, A2;

      hence thesis by Def2, A1;

    end;

    theorem :: RANDOM_1:30

    

     Th30: for Omega be non empty finite set, P be Probability of ( Trivial-SigmaField Omega), X be Real-Valued-Random-Variable of ( Trivial-SigmaField Omega) holds X is_integrable_on P

    proof

      let Omega be non empty finite set, P be Probability of ( Trivial-SigmaField Omega), X be Real-Valued-Random-Variable of ( Trivial-SigmaField Omega);

      set M = ( P2M P);

      

       A1: jj in REAL by XREAL_0:def 1;

      ( dom X) = Omega by FUNCT_2:def 1;

      then (M . ( dom X)) = jj by PROB_1:def 8;

      then (M . ( dom X)) < +infty by XXREAL_0: 9, A1;

      then X is_integrable_on M by Lm5, Th6;

      hence thesis;

    end;

    theorem :: RANDOM_1:31

    

     Th31: for Omega be non empty finite set, P be Probability of ( Trivial-SigmaField Omega), X be Real-Valued-Random-Variable of ( Trivial-SigmaField Omega), F be FinSequence of REAL , s be FinSequence of Omega st ( len F) = ( card Omega) & s is one-to-one & ( rng s) = Omega & ( len s) = ( card Omega) & (for n be Nat st n in ( dom F) holds (F . n) = ((X . (s . n)) * (P . {(s . n)}))) holds ( expect (X,P)) = ( Sum F)

    proof

      let Omega be non empty finite set, P be Probability of ( Trivial-SigmaField Omega), X be Real-Valued-Random-Variable of ( Trivial-SigmaField Omega), F be FinSequence of REAL , s be FinSequence of Omega;

      assume ( len F) = ( card Omega) & s is one-to-one & ( rng s) = Omega & ( len s) = ( card Omega) & for n be Nat st n in ( dom F) holds (F . n) = ((X . (s . n)) * (P . {(s . n)}));

      then ( Integral (( P2M P),X)) = ( Sum F) by Th12;

      hence thesis by Def4, Th30;

    end;

    theorem :: RANDOM_1:32

    for Omega be non empty finite set, P be Probability of ( Trivial-SigmaField Omega), X be Real-Valued-Random-Variable of ( Trivial-SigmaField Omega) holds ex F be FinSequence of REAL , s be FinSequence of Omega st ( len F) = ( card Omega) & s is one-to-one & ( rng s) = Omega & ( len s) = ( card Omega) & (for n be Nat st n in ( dom F) holds (F . n) = ((X . (s . n)) * (P . {(s . n)}))) & ( expect (X,P)) = ( Sum F)

    proof

      let Omega be non empty finite set, P be Probability of ( Trivial-SigmaField Omega), X be Real-Valued-Random-Variable of ( Trivial-SigmaField Omega);

      X is_integrable_on P & ex F be FinSequence of REAL , s be FinSequence of Omega st ( len F) = ( card Omega) & s is one-to-one & ( rng s) = Omega & ( len s) = ( card Omega) & (for n be Nat st n in ( dom F) holds (F . n) = ((X . (s . n)) * (P . {(s . n)}))) & ( Integral (( P2M P),X)) = ( Sum F) by Th13, Th30;

      hence thesis by Def4;

    end;

    theorem :: RANDOM_1:33

    

     Th33: for Omega be non empty finite set, P be Probability of ( Trivial-SigmaField Omega), X be Real-Valued-Random-Variable of ( Trivial-SigmaField Omega) holds ex F be FinSequence of REAL , s be FinSequence of Omega st ( len F) = ( card Omega) & s is one-to-one & ( rng s) = Omega & ( len s) = ( card Omega) & (for n be Nat st n in ( dom F) holds (F . n) = ((X . (s . n)) * (P . {(s . n)}))) & ( expect (X,P)) = ( Sum F)

    proof

      let Omega be non empty finite set, P be Probability of ( Trivial-SigmaField Omega), X be Real-Valued-Random-Variable of ( Trivial-SigmaField Omega);

      X is_integrable_on P & ex F be FinSequence of REAL , s be FinSequence of Omega st ( len F) = ( card Omega) & s is one-to-one & ( rng s) = Omega & ( len s) = ( card Omega) & (for n be Nat st n in ( dom F) holds (F . n) = ((X . (s . n)) * (P . {(s . n)}))) & ( Integral (( P2M P),X)) = ( Sum F) by Th13, Th30;

      hence thesis by Def4;

    end;

    theorem :: RANDOM_1:34

    for Omega be non empty finite set, X be Real-Valued-Random-Variable of ( Trivial-SigmaField Omega), G be FinSequence of REAL , s be FinSequence of Omega st ( len G) = ( card Omega) & s is one-to-one & ( rng s) = Omega & ( len s) = ( card Omega) & (for n be Nat st n in ( dom G) holds (G . n) = (X . (s . n))) holds ( expect (X,( Trivial-Probability Omega))) = (( Sum G) / ( card Omega))

    proof

      let Omega be non empty finite set, X be Real-Valued-Random-Variable of ( Trivial-SigmaField Omega), G be FinSequence of REAL , s be FinSequence of Omega;

      assume that

       A1: ( len G) = ( card Omega) and

       A2: s is one-to-one & ( rng s) = Omega and

       A3: ( len s) = ( card Omega) and

       A4: for n be Nat st n in ( dom G) holds (G . n) = (X . (s . n));

      set P = ( Trivial-Probability Omega);

      deffunc GF( Nat) = ( In (((X . (s . $1)) * (P . {(s . $1)})), REAL ));

      consider F be FinSequence of REAL such that

       A5: ( len F) = ( len G) & for j be Nat st j in ( dom F) holds (F . j) = GF(j) from FINSEQ_2:sch 1;

      

       A6: ( dom F) = ( dom G) by A5, FINSEQ_3: 29;

      reconsider cG = ((1 / ( card Omega)) (#) G) as FinSequence of REAL by RVSUM_1: 145;

      

       A7: ( dom F) = ( dom cG) by A6, VALUED_1:def 5;

      

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

      proof

        let n be Nat;

        assume

         A9: n in ( dom cG);

        ( dom s) = ( Seg ( len s)) by FINSEQ_1:def 3

        .= ( dom F) by A1, A3, A5, FINSEQ_1:def 3;

        then (s . n) in Omega by A9, PARTFUN1: 4, A7;

        then

        reconsider A = {(s . n)} as Singleton of Omega by RPR_1: 4;

        

         A10: (P . {(s . n)}) = ( prob A) by Def1

        .= (1 / ( card Omega)) by RPR_1: 14;

        

        thus (cG . n) = ((1 / ( card Omega)) * (G . n)) by VALUED_1: 6

        .= ((1 / ( card Omega)) * (X . (s . n))) by A4, A6, A9, A7

        .= GF(n) by A10

        .= (F . n) by A5, A9, A7;

      end;

      

       A11: for n be Nat st n in ( dom cG) holds (cG . n) = ((X . (s . n)) * (P . {(s . n)}))

      proof

        let n be Nat;

        assume

         A12: n in ( dom cG);

        ( dom s) = ( Seg ( len s)) by FINSEQ_1:def 3

        .= ( dom F) by A1, A3, A5, FINSEQ_1:def 3;

        then (s . n) in Omega by A12, PARTFUN1: 4, A7;

        then

        reconsider A = {(s . n)} as Singleton of Omega by RPR_1: 4;

        

         A13: (P . {(s . n)}) = ( prob A) by Def1

        .= (1 / ( card Omega)) by RPR_1: 14;

        

        thus (cG . n) = ((1 / ( card Omega)) * (G . n)) by VALUED_1: 6

        .= ((1 / ( card Omega)) * (X . (s . n))) by A4, A6, A12, A7

        .= GF(n) by A13

        .= ((X . (s . n)) * (P . {(s . n)}));

      end;

      ( dom F) = ( dom ((1 / ( card Omega)) (#) G)) by A6, VALUED_1:def 5;

      then

       A14: ((1 / ( card Omega)) (#) G) = F by FINSEQ_1: 13, A8;

      

       A15: ( len cG) = ( card Omega) by A1, A5, A14;

      

       A16: s is one-to-one by A2;

      ( rng s) = Omega & ( len s) = ( card Omega) by A2, A3;

      then ( expect (X,P)) = ( Sum cG) by Th31, A15, A16, A11;

      

      then ( expect (X,P)) = ( Sum cG)

      .= (( Sum G) / ( card Omega)) by RVSUM_1: 87;

      hence thesis;

    end;

    theorem :: RANDOM_1:35

    for Omega be non empty finite set, X be Real-Valued-Random-Variable of ( Trivial-SigmaField Omega) holds ex G be FinSequence of REAL , s be FinSequence of Omega st ( len G) = ( card Omega) & s is one-to-one & ( rng s) = Omega & ( len s) = ( card Omega) & (for n be Nat st n in ( dom G) holds (G . n) = (X . (s . n))) & ( expect (X,( Trivial-Probability Omega))) = (( Sum G) / ( card Omega))

    proof

      let Omega be non empty finite set, X be Real-Valued-Random-Variable of ( Trivial-SigmaField Omega);

      set P = ( Trivial-Probability Omega);

      consider F be FinSequence of REAL , s be FinSequence of Omega such that

       A1: ( len F) = ( card Omega) and

       A2: s is one-to-one & ( rng s) = Omega and

       A3: ( len s) = ( card Omega) and

       A4: for n be Nat st n in ( dom F) holds (F . n) = ((X . (s . n)) * (P . {(s . n)})) and

       A5: ( expect (X,P)) = ( Sum F) by Th33;

      deffunc GF( Nat) = ( In ((X . (s . $1)), REAL ));

      consider G be FinSequence of REAL such that

       A6: ( len G) = ( len F) & for j be Nat st j in ( dom G) holds (G . j) = GF(j) from FINSEQ_2:sch 1;

      

       A7: ( dom F) = ( dom G) by A6, FINSEQ_3: 29;

       A8:

      now

        let n be Nat;

        assume

         A9: n in ( dom F);

        ( dom s) = ( Seg ( len s)) by FINSEQ_1:def 3

        .= ( dom F) by A1, A3, FINSEQ_1:def 3;

        then (s . n) in Omega by A9, PARTFUN1: 4;

        then

        reconsider A = {(s . n)} as Singleton of Omega by RPR_1: 4;

        

         A10: (P . {(s . n)}) = ( prob A) by Def1

        .= (1 / ( card Omega)) by RPR_1: 14;

        

        thus (((1 / ( card Omega)) (#) G) . n) = ((1 / ( card Omega)) * (G . n)) by VALUED_1: 6

        .= ((1 / ( card Omega)) * GF(n)) by A6, A7, A9

        .= ((1 / ( card Omega)) * (X . (s . n)))

        .= ((X . (s . n)) * (P . {(s . n)})) by A10

        .= (F . n) by A4, A9;

      end;

      take G, s;

      ( dom F) = ( dom ((1 / ( card Omega)) (#) G)) by A7, VALUED_1:def 5;

      then

       A11: ((1 / ( card Omega)) (#) G) = F by A8, FINSEQ_1: 13;

      thus ( len G) = ( card Omega) & s is one-to-one & ( rng s) = Omega & ( len s) = ( card Omega) by A1, A2, A3, A6;

      thus for n be Nat st n in ( dom G) holds (G . n) = (X . (s . n))

      proof

        let n be Nat;

        assume n in ( dom G);

        then (G . n) = GF(n) by A6;

        hence thesis;

      end;

      thus thesis by A5, RVSUM_1: 87, A11;

    end;

    theorem :: RANDOM_1:36

    for X be Real-Valued-Random-Variable of Sigma st 0 < r & X is nonnegative & X is_integrable_on P holds (P . { t where t be Element of Omega : r <= (X . t) }) <= (( expect (X,P)) / r)

    proof

      let X be Real-Valued-Random-Variable of Sigma;

      assume that

       A1: 0 < r and

       A2: X is nonnegative and

       A3: X is_integrable_on P;

      set PM = ( P2M P);

      set K = { t where t be Element of Omega : r <= (X . t) };

      set S = ( [#] Sigma);

      

       A5: X is S -measurable by Def2;

      now

        let t be object;

        assume t in (S /\ ( great_eq_dom (X,r)));

        then t in ( great_eq_dom (X,r)) by XBOOLE_0:def 4;

        then t in ( dom X) & r <= (X . t) by MESFUNC1:def 14;

        hence t in K;

      end;

      then

       A6: (S /\ ( great_eq_dom (X,r))) c= K;

      

       A7: ( dom X) = S by FUNCT_2:def 1;

      now

        let x be object;

        assume x in K;

        then

         A8: ex t be Element of Omega st x = t & r <= (X . t);

        then x in ( great_eq_dom (X,r)) by A7, MESFUNC1:def 14;

        hence x in (S /\ ( great_eq_dom (X,r))) by A8, XBOOLE_0:def 4;

      end;

      then K c= (S /\ ( great_eq_dom (X,r)));

      then (S /\ ( great_eq_dom (X,r))) = K by A6;

      then

      reconsider K as Element of Sigma by A5, A7, MESFUNC6: 13;

      ( Integral (PM,(X | K))) <= ( Integral (PM,(X | S))) by A2, A5, A7, MESFUNC6: 87;

      then

       A9: ( Integral (PM,(X | K))) <= ( Integral (PM,X));

      ( expect (X,P)) = ( Integral (PM,X)) by A3, Def4;

      then

      reconsider IX = ( Integral (PM,X)) as Element of REAL by XREAL_0:def 1;

      reconsider PMK = (PM . K) as Element of REAL by XXREAL_0: 14;

      

       A10: for t be Element of Omega st t in K holds r <= (X . t)

      proof

        let t be Element of Omega;

        assume t in K;

        then ex s be Element of Omega st s = t & r <= (X . s);

        hence thesis;

      end;

      

       A11: jj in REAL by XREAL_0:def 1;

      (PM . K) <= jj by PROB_1: 35;

      then

       A12: (PM . K) < +infty by XXREAL_0: 2, XXREAL_0: 9, A11;

      X is_integrable_on ( P2M P) by A3;

      then (r * (PM . K)) <= ( Integral (PM,(X | K))) by A7, A12, A10, Th2;

      then (r * PMK) <= ( Integral (PM,(X | K))) by EXTREAL1: 1;

      then (r * PMK) <= ( Integral (PM,X)) by A9, XXREAL_0: 2;

      then ((r * PMK) / r) <= (IX / r) by A1, XREAL_1: 72;

      then PMK <= (IX / r) by A1, XCMPLX_1: 89;

      hence thesis by A3, Def4;

    end;