random_2.miz



    begin

    reserve Omega for non empty set;

    reserve r for Real;

    reserve Sigma for SigmaField of Omega;

    reserve P for Probability of Sigma;

    theorem :: RANDOM_2:1

    

     Th1: for f be one-to-one Function, A,B be Subset of ( dom f) st A misses B holds ( rng (f | A)) misses ( rng (f | B))

    proof

      let f be one-to-one Function, A,B be Subset of ( dom f);

      assume

       A1: A misses B;

      assume ( rng (f | A)) meets ( rng (f | B));

      then

      consider y be object such that

       A2: y in ( rng (f | A)) & y in ( rng (f | B)) by XBOOLE_0: 3;

      consider xa be object such that

       A3: xa in ( dom (f | A)) & y = ((f | A) . xa) by A2, FUNCT_1:def 3;

      consider xb be object such that

       A4: xb in ( dom (f | B)) & y = ((f | B) . xb) by A2, FUNCT_1:def 3;

      

       A5: xa in ( dom f) & xb in ( dom f) by A3, A4, RELAT_1: 57;

      y = (f . xa) & y = (f . xb) by A3, A4, FUNCT_1: 47;

      then

       A6: xa = xb by A5, FUNCT_1:def 4;

      ( dom (f | A)) c= A & ( dom (f | B)) c= B by RELAT_1: 58;

      then xa in (A /\ B) by A6, A3, A4, XBOOLE_0:def 4;

      hence contradiction by A1, XBOOLE_0: 4;

    end;

    theorem :: RANDOM_2:2

    

     Th2: for f,g be Function holds ( rng (f * g)) c= ( rng (f | ( rng g)))

    proof

      let f,g be Function;

      let y be object;

      assume y in ( rng (f * g));

      then

      consider x be object such that

       A1: x in ( dom (f * g)) & y = ((f * g) . x) by FUNCT_1:def 3;

      

       A2: x in ( dom g) & (g . x) in ( dom f) by A1, FUNCT_1: 11;

      reconsider z = (g . x) as set;

      (f . z) in ( rng (f | ( rng g))) by A2, FUNCT_1: 3, FUNCT_1: 50;

      hence thesis by A1, FUNCT_1: 12;

    end;

    registration

      let Omega, Sigma;

      cluster nonnegative for Real-Valued-Random-Variable of Sigma;

      existence

      proof

        set X = the Real-Valued-Random-Variable of Sigma;

        now

          let x be object;

          assume x in ( dom ( abs X));

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

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

        end;

        then ( abs X) is nonnegative by MESFUNC6: 52;

        hence thesis;

      end;

    end

    registration

      let Omega, Sigma;

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

      cluster ( abs X) -> nonnegative;

      coherence

      proof

        now

          let x be object;

          assume x in ( dom ( abs X));

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

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

        end;

        hence thesis by MESFUNC6: 52;

      end;

    end

    theorem :: RANDOM_2:3

    

     Th3: (Omega --> 1) = ( chi (Omega,Omega))

    proof

      set E0 = (Omega --> 1);

      

       A1: ( dom ( chi (Omega,Omega))) = Omega by FUNCT_3:def 3;

      

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

      now

        let x be object;

        assume

         A3: x in ( dom ( chi (Omega,Omega)));

        per cases ;

          suppose x in Omega;

          

          hence (( chi (Omega,Omega)) . x) = 1 by FUNCT_3:def 3

          .= (E0 . x) by A3, FUNCOP_1: 7;

        end;

          suppose not x in Omega;

          hence (( chi (Omega,Omega)) . x) = (E0 . x) by A3;

        end;

      end;

      hence thesis by A1, A2, FUNCT_1: 2;

    end;

    theorem :: RANDOM_2:4

    

     Th4: (Omega --> r) is Real-Valued-Random-Variable of Sigma

    proof

      set E0 = (Omega --> 1);

      set E = (Omega --> r);

      reconsider S = Omega as Element of Sigma by MEASURE1: 7;

      

       A1: ( dom E0) = Omega & ( rng E0) c= {1} by FUNCOP_1: 13;

      reconsider E0 as Function of Omega, REAL by FUNCT_2: 7, NUMBERS: 19;

      

       A2: ( R_EAL E0) = ( chi (S,Omega)) by Th3;

      ( chi (S,Omega)) is S -measurable by MESFUNC2: 29;

      then E0 is ( [#] Sigma) -measurable by A2, MESFUNC6:def 1;

      then

       A3: E0 is Real-Valued-Random-Variable of Sigma by RANDOM_1:def 2;

      

       A4: ( dom E) = ( dom E0) by A1, FUNCT_2:def 1;

      now

        let x be object;

        assume

         A5: x in ( dom E);

        

        hence (E . x) = (r * 1) by FUNCOP_1: 7

        .= (r * (E0 . x)) by A5, FUNCOP_1: 7;

      end;

      then E = (r (#) E0) by A4, VALUED_1:def 5;

      hence thesis by A3, RANDOM_1: 20;

    end;

    theorem :: RANDOM_2:5

    

     Th5: for X be non empty set, f be PartFunc of X, REAL holds (f to_power 2) = (( - f) to_power 2) & (f to_power 2) = (( abs f) to_power 2)

    proof

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

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

      then ( dom (( - f) to_power 2)) = ( dom f) by MESFUN6C:def 4;

      then

       A1: ( dom (f to_power 2)) = ( dom (( - f) to_power 2)) by MESFUN6C:def 4;

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

      then

       A2: ( dom (( abs f) to_power 2)) = ( dom f) by MESFUN6C:def 4;

      then

       A3: ( dom (f to_power 2)) = ( dom (( abs f) to_power 2)) by MESFUN6C:def 4;

      for x be Element of X st x in ( dom (f to_power 2)) holds ((f to_power 2) . x) = ((( - f) to_power 2) . x) & ((f to_power 2) . x) = ((( abs f) to_power 2) . x)

      proof

        let x be Element of X;

        assume

         A4: x in ( dom (f to_power 2));

        then

         A5: x in ( dom (( - f) to_power 2)) & x in ( dom (f to_power 2)) & x in ( dom f) & x in ( dom ( - f)) & x in ( dom (( abs f) to_power 2)) by A2, A1, MESFUN6C:def 4;

        

         A6: ((( - f) to_power 2) . x) = ((( - f) . x) to_power 2) by A4, A1, MESFUN6C:def 4

        .= (( - (f . x)) to_power 2) by VALUED_1: 8

        .= ((f . x) to_power 2) by FIB_NUM3: 3

        .= ((f to_power 2) . x) by A4, MESFUN6C:def 4;

        ((( abs f) to_power 2) . x) = ((f to_power 2) . x)

        proof

          

           A7: ((( abs f) to_power 2) . x) = ((( abs f) . x) to_power 2) by A5, MESFUN6C:def 4

          .= ( |.(f . x) qua Complex.| to_power 2) by VALUED_1: 18;

          now

            per cases by A7, ABSVALUE: 1;

              case ((( abs f) to_power 2) . x) = ((f . x) to_power 2);

              hence thesis by A4, MESFUN6C:def 4;

            end;

              case ((( abs f) to_power 2) . x) = (( - (f . x)) to_power 2);

              

              then ((( abs f) to_power 2) . x) = ((f . x) to_power 2) by FIB_NUM3: 3

              .= ((f to_power 2) . x) by A4, MESFUN6C:def 4;

              hence thesis;

            end;

          end;

          hence thesis;

        end;

        hence thesis by A6;

      end;

      then (for x be Element of X st x in ( dom (f to_power 2)) holds ((f to_power 2) . x) = ((( - f) to_power 2) . x)) & (for x be Element of X st x in ( dom (f to_power 2)) holds ((f to_power 2) . x) = ((( abs f) to_power 2) . x));

      hence thesis by A1, A3, PARTFUN1: 5;

    end;

    theorem :: RANDOM_2:6

    

     Th6: for X be non empty set, f,g be PartFunc of X, REAL holds ((f + g) to_power 2) = (((f to_power 2) + (2 (#) (f (#) g))) + (g to_power 2)) & ((f - g) to_power 2) = (((f to_power 2) - (2 (#) (f (#) g))) + (g to_power 2))

    proof

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

      

       A1: ( dom (f to_power 2)) = ( dom f) & for x be Element of X st x in ( dom (f to_power 2)) holds ((f to_power 2) . x) = ((f . x) to_power 2) by MESFUN6C:def 4;

      

       A2: ( dom (g to_power 2)) = ( dom g) & for x be Element of X st x in ( dom (g to_power 2)) holds ((g to_power 2) . x) = ((g . x) to_power 2) by MESFUN6C:def 4;

      

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

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

       A4:

      now

        let x be Element of X;

        assume x in (( dom f) /\ ( dom g));

        

        thus ((2 (#) (f (#) g)) . x) = (2 * ((f (#) g) . x)) by VALUED_1: 6

        .= (2 * ((f . x) * (g . x))) by VALUED_1: 5

        .= ((2 * (f . x)) * (g . x));

      end;

      

       A5: ( dom ((f + g) to_power 2)) = ( dom (f + g)) by MESFUN6C:def 4

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

      

       A6: ( dom ((f - g) to_power 2)) = ( dom (f - g)) by MESFUN6C:def 4

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

      

       A7: ( dom ((f to_power 2) + (2 (#) (f (#) g)))) = (( dom f) /\ ( dom (2 (#) (f (#) g)))) by A1, VALUED_1:def 1

      .= (( dom f) /\ ( dom g)) by A3, XBOOLE_1: 17, XBOOLE_1: 28;

      

       A8: ( dom ((f to_power 2) - (2 (#) (f (#) g)))) = (( dom f) /\ ( dom (2 (#) (f (#) g)))) by A1, VALUED_1: 12

      .= (( dom f) /\ ( dom g)) by A3, XBOOLE_1: 17, XBOOLE_1: 28;

      

       A9: ( dom (((f to_power 2) + (2 (#) (f (#) g))) + (g to_power 2))) = (( dom ((f to_power 2) + (2 (#) (f (#) g)))) /\ ( dom g)) by A2, VALUED_1:def 1

      .= ((( dom f) /\ ( dom (2 (#) (f (#) g)))) /\ ( dom g)) by A1, VALUED_1:def 1

      .= ((( dom f) /\ ( dom g)) /\ ( dom g)) by A3, XBOOLE_1: 17, XBOOLE_1: 28

      .= (( dom f) /\ ( dom g)) by XBOOLE_1: 17, XBOOLE_1: 28;

      

       A10: ( dom (((f to_power 2) - (2 (#) (f (#) g))) + (g to_power 2))) = (( dom ((f to_power 2) - (2 (#) (f (#) g)))) /\ ( dom g)) by A2, VALUED_1:def 1

      .= (( dom f) /\ ( dom g)) by A8, XBOOLE_1: 17, XBOOLE_1: 28;

      now

        let x be Element of X;

        assume

         A11: x in (( dom f) /\ ( dom g));

        then

         A12: x in ( dom (f + g)) by VALUED_1:def 1;

        

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

        

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

        

         A15: x in ( dom (f - g)) by A11, VALUED_1: 12;

        then

         A16: x in ( dom ((f - g) to_power 2)) by MESFUN6C:def 4;

        

         A17: (((f + g) to_power 2) . x) = (((f + g) . x) to_power 2) by A11, A5, MESFUN6C:def 4

        .= (((f . x) + (g . x)) to_power 2) by A12, VALUED_1:def 1

        .= (((f . x) + (g . x)) ^2 ) by POWER: 46

        .= ((((f . x) ^2 ) + ((2 * (f . x)) * (g . x))) + ((g . x) ^2 ))

        .= ((((f . x) to_power 2) + ((2 * (f . x)) * (g . x))) + ((g . x) ^2 )) by POWER: 46

        .= ((((f . x) to_power 2) + ((2 * (f . x)) * (g . x))) + ((g . x) to_power 2)) by POWER: 46

        .= ((((f to_power 2) . x) + ((2 * (f . x)) * (g . x))) + ((g . x) to_power 2)) by A1, A13

        .= ((((f to_power 2) . x) + ((2 * (f . x)) * (g . x))) + ((g to_power 2) . x)) by A2, A14

        .= ((((f to_power 2) . x) + ((2 (#) (f (#) g)) . x)) + ((g to_power 2) . x)) by A4, A11

        .= ((((f to_power 2) + (2 (#) (f (#) g))) . x) + ((g to_power 2) . x)) by A7, A11, VALUED_1:def 1

        .= ((((f to_power 2) + (2 (#) (f (#) g))) + (g to_power 2)) . x) by A9, A11, VALUED_1:def 1;

        (((f - g) to_power 2) . x) = (((f - g) . x) to_power 2) by A16, MESFUN6C:def 4

        .= (((f . x) - (g . x)) to_power 2) by A15, VALUED_1: 13

        .= (((f . x) - (g . x)) ^2 ) by POWER: 46

        .= ((((f . x) ^2 ) - ((2 * (f . x)) * (g . x))) + ((g . x) ^2 ))

        .= ((((f . x) to_power 2) - ((2 * (f . x)) * (g . x))) + ((g . x) ^2 )) by POWER: 46

        .= ((((f . x) to_power 2) - ((2 * (f . x)) * (g . x))) + ((g . x) to_power 2)) by POWER: 46

        .= ((((f to_power 2) . x) - ((2 * (f . x)) * (g . x))) + ((g . x) to_power 2)) by A1, A13

        .= ((((f to_power 2) . x) - ((2 * (f . x)) * (g . x))) + ((g to_power 2) . x)) by A2, A14

        .= ((((f to_power 2) . x) - ((2 (#) (f (#) g)) . x)) + ((g to_power 2) . x)) by A4, A11

        .= ((((f to_power 2) - (2 (#) (f (#) g))) . x) + ((g to_power 2) . x)) by A8, A11, VALUED_1: 13

        .= ((((f to_power 2) - (2 (#) (f (#) g))) + (g to_power 2)) . x) by A10, A11, VALUED_1:def 1;

        hence (((f + g) to_power 2) . x) = ((((f to_power 2) + (2 (#) (f (#) g))) + (g to_power 2)) . x) & (((f - g) to_power 2) . x) = ((((f to_power 2) - (2 (#) (f (#) g))) + (g to_power 2)) . x) by A17;

      end;

      then (for x be Element of X st x in ( dom ((f + g) to_power 2)) holds (((f + g) to_power 2) . x) = ((((f to_power 2) + (2 (#) (f (#) g))) + (g to_power 2)) . x)) & (for x be Element of X st x in ( dom ((f - g) to_power 2)) holds (((f - g) to_power 2) . x) = ((((f to_power 2) - (2 (#) (f (#) g))) + (g to_power 2)) . x)) by A5, A6;

      hence thesis by A5, A9, A10, A6, PARTFUN1: 5;

    end;

    definition

      let Omega, Sigma, P;

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

      assume

       A1: X is_integrable_on P & (( abs X) to_power 2) is_integrable_on ( P2M P);

      :: RANDOM_2:def1

      func variance (X,P) -> Real means

      : Def1: ex Y be Real-Valued-Random-Variable of Sigma, E be Real-Valued-Random-Variable of Sigma st E = (Omega --> ( expect (X,P))) & Y = (X - E) & Y is_integrable_on P & (( abs Y) to_power 2) is_integrable_on ( P2M P) & it = ( Integral (( P2M P),(( abs Y) to_power 2)));

      correctness

      proof

        set S = ( [#] Sigma);

        

         A3: 1 in REAL by XREAL_0:def 1;

        (( P2M P) . S) <= 1 by PROB_1: 35;

        then

         A4: (( P2M P) . S) < +infty by XXREAL_0: 2, XXREAL_0: 9, A3;

        set r = ( expect (X,P));

        set E0 = (Omega --> 1);

        set E = (Omega --> ( expect (X,P)));

        

         A5: ( dom E0) = Omega & ( rng E0) c= {1} by FUNCOP_1: 13;

        reconsider E0 as Real-Valued-Random-Variable of Sigma by Th4;

        

         A6: ( R_EAL E0) = ( chi (S,Omega)) by Th3;

        

         A7: ( dom E) = ( dom E0) by A5, FUNCT_2:def 1;

        now

          let x be object;

          assume

           A8: x in ( dom E);

          

          hence (E . x) = (r * 1) by FUNCOP_1: 7

          .= (r * (E0 . x)) by A8, FUNCOP_1: 7;

        end;

        then

         A9: E = (r (#) E0) by A7, VALUED_1:def 5;

        reconsider E as Real-Valued-Random-Variable of Sigma by Th4;

        set Y = (X - E);

        reconsider Y as Real-Valued-Random-Variable of Sigma;

        ( chi (S,Omega)) is_integrable_on ( P2M P) by A4, MESFUNC7: 24;

        then

         A10: E0 is_integrable_on ( P2M P) by A6, MESFUNC6:def 4;

        then

         A11: (r (#) E0) is_integrable_on ( P2M P) by MESFUNC6: 102;

        

         A12: (( - 1) (#) (r (#) E0)) is_integrable_on ( P2M P) by A11, MESFUNC6: 102;

        

         A13: X is_integrable_on ( P2M P) by A1, RANDOM_1:def 3;

        then Y is_integrable_on ( P2M P) by A9, A12, MESFUNC6: 100;

        then

         A14: Y is_integrable_on P by RANDOM_1:def 3;

        ((2 * r) (#) X) is_integrable_on ( P2M P) by A13, MESFUNC6: 102;

        then (( - 1) (#) ((2 * r) (#) X)) is_integrable_on ( P2M P) by MESFUNC6: 102;

        then

         A15: ((( abs X) to_power 2) - ((2 * r) (#) X)) is_integrable_on ( P2M P) by A1, MESFUNC6: 100;

        

         A16: (((X to_power 2) - (2 (#) ((r (#) E0) (#) X))) + ((r (#) E0) to_power 2)) = (((X to_power 2) - ((2 * r) (#) X)) + ((r * r) (#) E0))

        proof

          

           A17: ( dom (X to_power 2)) = ( dom X) by MESFUN6C:def 4;

          

           A18: ( dom (2 (#) ((r (#) E0) (#) X))) = ( dom ((r (#) E0) (#) X)) by VALUED_1:def 5

          .= (( dom (r (#) E0)) /\ ( dom X)) by VALUED_1:def 4

          .= (Omega /\ ( dom X)) by A5, VALUED_1:def 5;

          

           A19: ( dom ((r (#) E0) to_power 2)) = ( dom (r (#) E0)) by MESFUN6C:def 4

          .= Omega by A5, VALUED_1:def 5;

          

           A20: ( dom ((r * r) (#) E0)) = Omega by A5, VALUED_1:def 5;

          

           A21: ( dom ((2 * r) (#) X)) = ( dom X) by VALUED_1:def 5;

          

           A22: ( dom ((X to_power 2) - (2 (#) ((r (#) E0) (#) X)))) = (( dom X) /\ (Omega /\ ( dom X))) by A17, A18, VALUED_1: 12

          .= ((( dom X) /\ ( dom X)) /\ Omega) by XBOOLE_1: 16

          .= (( dom X) /\ Omega);

          

           A23: ( dom ((X to_power 2) - ((2 * r) (#) X))) = (( dom (X to_power 2)) /\ ( dom ((2 * r) (#) X))) by VALUED_1: 12

          .= ( dom X) by A17, A21;

          

           A24: ( dom (((X to_power 2) - (2 (#) ((r (#) E0) (#) X))) + ((r (#) E0) to_power 2))) = (( dom ((X to_power 2) - (2 (#) ((r (#) E0) (#) X)))) /\ ( dom ((r (#) E0) to_power 2))) by VALUED_1:def 1

          .= (( dom X) /\ (Omega /\ Omega)) by A19, A22, XBOOLE_1: 16

          .= (( dom X) /\ Omega);

          then

           A25: ( dom (((X to_power 2) - (2 (#) ((r (#) E0) (#) X))) + ((r (#) E0) to_power 2))) = ( dom (((X to_power 2) - ((2 * r) (#) X)) + ((r * r) (#) E0))) by A20, A23, VALUED_1:def 1;

          for x be Element of Omega st x in ( dom (((X to_power 2) - (2 (#) ((r (#) E0) (#) X))) + ((r (#) E0) to_power 2))) holds ((((X to_power 2) - (2 (#) ((r (#) E0) (#) X))) + ((r (#) E0) to_power 2)) . x) = ((((X to_power 2) - ((2 * r) (#) X)) + ((r * r) (#) E0)) . x)

          proof

            let x be Element of Omega;

            assume

             A26: x in ( dom (((X to_power 2) - (2 (#) ((r (#) E0) (#) X))) + ((r (#) E0) to_power 2)));

            then

             A27: x in ( dom X) & x in Omega by A24, XBOOLE_0:def 4;

            

             A28: ((((X to_power 2) - (2 (#) ((r (#) E0) (#) X))) + ((r (#) E0) to_power 2)) . x) = ((((X to_power 2) - (2 (#) ((r (#) E0) (#) X))) . x) + (((r (#) E0) to_power 2) . x)) by A26, VALUED_1:def 1

            .= ((((X to_power 2) . x) - ((2 (#) ((r (#) E0) (#) X)) . x)) + (((r (#) E0) to_power 2) . x)) by A22, A24, A26, VALUED_1: 13

            .= ((((X to_power 2) . x) - (2 * (((r (#) E0) (#) X) . x))) + (((r (#) E0) to_power 2) . x)) by VALUED_1: 6

            .= ((((X to_power 2) . x) - (2 * (((r (#) E0) . x) * (X . x)))) + (((r (#) E0) to_power 2) . x)) by VALUED_1: 5

            .= ((((X to_power 2) . x) - (2 * ((r * (E0 . x)) * (X . x)))) + (((r (#) E0) to_power 2) . x)) by VALUED_1: 6

            .= ((((X to_power 2) . x) - (2 * ((r * 1) * (X . x)))) + (((r (#) E0) to_power 2) . x)) by FUNCOP_1: 7

            .= ((((X to_power 2) . x) - ((2 * r) * (X . x))) + (((r (#) E0) . x) to_power 2)) by A19, MESFUN6C:def 4

            .= ((((X to_power 2) . x) - ((2 * r) * (X . x))) + ((r * (E0 . x)) to_power 2)) by VALUED_1: 6

            .= ((((X to_power 2) . x) - ((2 * r) * (X . x))) + ((r * 1) to_power 2)) by FUNCOP_1: 7

            .= ((((X to_power 2) . x) - ((2 * r) * (X . x))) + (r ^2 )) by POWER: 46

            .= ((((X to_power 2) . x) - ((2 * r) * (X . x))) + (r * r));

            ((((X to_power 2) - ((2 * r) (#) X)) + ((r * r) (#) E0)) . x) = ((((X to_power 2) - ((2 * r) (#) X)) . x) + (((r * r) (#) E0) . x)) by A26, A25, VALUED_1:def 1

            .= ((((X to_power 2) . x) - (((2 * r) (#) X) . x)) + (((r * r) (#) E0) . x)) by A23, A27, VALUED_1: 13

            .= ((((X to_power 2) . x) - ((2 * r) * (X . x))) + (((r * r) (#) E0) . x)) by VALUED_1: 6

            .= ((((X to_power 2) . x) - ((2 * r) * (X . x))) + ((r * r) * (E0 . x))) by VALUED_1: 6

            .= ((((X to_power 2) . x) - ((2 * r) * (X . x))) + ((r * r) * 1)) by FUNCOP_1: 7

            .= ((((X to_power 2) . x) - ((2 * r) * (X . x))) + (r * r));

            hence thesis by A28;

          end;

          hence thesis by A25, PARTFUN1: 5;

        end;

        

         A29: (( abs Y) to_power 2) = ((X - (r (#) E0)) to_power 2) by Th5, A9

        .= (((X to_power 2) - (2 (#) ((r (#) E0) (#) X))) + ((r (#) E0) to_power 2)) by Th6

        .= (((( abs X) to_power 2) - ((2 * r) (#) X)) + ((r * r) (#) E0)) by Th5, A16;

        

         A30: ((r * r) (#) E0) is_integrable_on ( P2M P) by A10, MESFUNC6: 102;

        then (( abs Y) to_power 2) is_integrable_on ( P2M P) by A15, A29, MESFUNC6: 100;

        then -infty < ( Integral (( P2M P),(( abs Y) to_power 2))) & ( Integral (( P2M P),(( abs Y) to_power 2))) < +infty by MESFUNC6: 90;

        then ( Integral (( P2M P),(( abs Y) to_power 2))) is Element of REAL by XXREAL_0: 14;

        hence thesis by A30, A15, A29, A14, MESFUNC6: 100;

      end;

    end

    begin

    theorem :: RANDOM_2:7

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

    proof

      let Omega, Sigma, P, r;

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

      assume

       A1: 0 < r & X is nonnegative & X is_integrable_on P & (( abs X) to_power 2) is_integrable_on ( P2M P);

      

       A2: { t where t be Element of Omega : r <= |.((X . t) - ( expect (X,P))) qua Complex.| } c= { t where t be Element of Omega : (r to_power 2) <= ( |.((X . t) - ( expect (X,P))) qua Complex.| to_power 2) }

      proof

        let s be object;

        assume s in { t where t be Element of Omega : r <= |.((X . t) - ( expect (X,P))) qua Complex.| };

        then

         A3: ex ss be Element of Omega st s = ss & r <= |.((X . ss) - ( expect (X,P))) qua Complex.|;

        

         A4: (r ^2 ) = (r to_power 2) & ( |.((X . s) - ( expect (X,P))) qua Complex.| ^2 ) = ( |.((X . s) - ( expect (X,P))) qua Complex.| to_power 2) by POWER: 46;

        (r ^2 ) <= ( |.((X . s) - ( expect (X,P))) qua Complex.| ^2 ) by A1, A3, SQUARE_1: 15;

        hence thesis by A3, A4;

      end;

      { t where t be Element of Omega : (r to_power 2) <= ( |.((X . t) - ( expect (X,P))) qua Complex.| to_power 2) } c= { t where t be Element of Omega : r <= |.((X . t) - ( expect (X,P))) qua Complex.| }

      proof

        let s be object;

        assume s in { t where t be Element of Omega : (r to_power 2) <= ( |.((X . t) - ( expect (X,P))) qua Complex.| to_power 2) };

        then

         A5: ex ss be Element of Omega st s = ss & (r to_power 2) <= ( |.((X . ss) - ( expect (X,P))) qua Complex.| to_power 2);

        

         A6: 0 <= |.((X . s) - ( expect (X,P))) qua Complex.| by COMPLEX1: 46;

        (r ^2 ) = (r to_power 2) & ( |.((X . s) - ( expect (X,P))) qua Complex.| ^2 ) = ( |.((X . s) - ( expect (X,P))) qua Complex.| to_power 2) by POWER: 46;

        then r <= |.((X . s) - ( expect (X,P))) qua Complex.| by A6, A5, SQUARE_1: 47;

        hence thesis by A5;

      end;

      then

       A7: { t where t be Element of Omega : r <= |.((X . t) - ( expect (X,P))) qua Complex.| } = { t where t be Element of Omega : (r to_power 2) <= ( |.((X . t) - ( expect (X,P))) qua Complex.| to_power 2) } by A2, XBOOLE_0:def 10;

      consider Y be Real-Valued-Random-Variable of Sigma, E be Real-Valued-Random-Variable of Sigma such that

       A8: E = (Omega --> ( expect (X,P))) & Y = (X - E) & Y is_integrable_on P & (( abs Y) to_power 2) is_integrable_on ( P2M P) & ( variance (X,P)) = ( Integral (( P2M P),(( abs Y) to_power 2))) by Def1, A1;

      reconsider Z = (( abs Y) to_power 2) as Real-Valued-Random-Variable of Sigma by RANDOM_1: 23;

      

       A9: Z is_integrable_on P by A8, RANDOM_1:def 3;

      then

       A10: (P . { t where t be Element of Omega : (r to_power 2) <= (Z . t) }) <= (( expect (Z,P)) / (r to_power 2)) by A1, POWER: 34, RANDOM_1: 36;

      

       A11: ( expect (Z,P)) = ( variance (X,P)) by A8, A9, RANDOM_1:def 4;

      

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

      

       A13: ( dom (Omega --> ( expect (X,P)))) = Omega by FUNCOP_1: 13;

      

       A14: ( dom (X - (Omega --> ( expect (X,P))))) = (( dom X) /\ ( dom (Omega --> ( expect (X,P))))) by VALUED_1: 12

      .= Omega by A12, A13;

      then

       A15: ( dom |.(X - (Omega --> ( expect (X,P)))).|) = Omega by VALUED_1:def 11;

      then

       A16: ( dom ( |.(X - (Omega --> ( expect (X,P)))).| to_power 2)) = Omega by MESFUN6C:def 4;

      

       A17: { t where t be Element of Omega : (r to_power 2) <= ( |.((X . t) - ( expect (X,P))) qua Complex.| to_power 2) } c= { t where t be Element of Omega : (r to_power 2) <= (Z . t) }

      proof

        let s be object;

        assume s in { t where t be Element of Omega : (r to_power 2) <= ( |.((X . t) - ( expect (X,P))) qua Complex.| to_power 2) };

        then

         A18: ex ss be Element of Omega st s = ss & (r to_power 2) <= ( |.((X . ss) - ( expect (X,P))) qua Complex.| to_power 2);

        

        then (Z . s) = (( |.(X - (Omega --> ( expect (X,P)))).| . s) to_power 2) by A16, A8, MESFUN6C:def 4

        .= ( |.((X - (Omega --> ( expect (X,P)))) . s) qua Complex.| to_power 2) by A15, A18, VALUED_1:def 11

        .= ( |.((X . s) - ((Omega --> ( expect (X,P))) . s)) qua Complex.| to_power 2) by A14, A18, VALUED_1: 13

        .= ( |.((X . s) - ( expect (X,P))) qua Complex.| to_power 2) by A18, FUNCOP_1: 7;

        hence thesis by A18;

      end;

      { t where t be Element of Omega : (r to_power 2) <= (Z . t) } c= { t where t be Element of Omega : (r to_power 2) <= ( |.((X . t) - ( expect (X,P))) qua Complex.| to_power 2) }

      proof

        let s be object;

        assume s in { t where t be Element of Omega : (r to_power 2) <= (Z . t) };

        then

         A19: ex ss be Element of Omega st s = ss & (r to_power 2) <= (Z . ss);

        

        then (Z . s) = (( |.(X - (Omega --> ( expect (X,P)))).| . s) to_power 2) by A16, A8, MESFUN6C:def 4

        .= ( |.((X - (Omega --> ( expect (X,P)))) . s) qua Complex.| to_power 2) by A15, A19, VALUED_1:def 11

        .= ( |.((X . s) - ((Omega --> ( expect (X,P))) . s)) qua Complex.| to_power 2) by A14, A19, VALUED_1: 13

        .= ( |.((X . s) - ( expect (X,P))) qua Complex.| to_power 2) by A19, FUNCOP_1: 7;

        hence thesis by A19;

      end;

      hence thesis by A11, A10, A7, A17, XBOOLE_0:def 10;

    end;

    begin

    theorem :: RANDOM_2:8

    

     Th8: for Omega be non empty finite set, f be Function of Omega, REAL , P be Function of ( bool Omega), REAL st (for x be set st x c= Omega holds 0 <= (P . x) & (P . x) <= 1) & (P . Omega) = 1 & for z be finite Subset of Omega holds (P . z) = ( setopfunc (z,Omega, REAL ,f, addreal )) holds P is Probability of ( Trivial-SigmaField Omega)

    proof

      let Omega be non empty finite set, f be Function of Omega, REAL , P be Function of ( bool Omega), REAL ;

      assume that

       A1: for x be set st x c= Omega holds 0 <= (P . x) & (P . x) <= 1 and

       A2: (P . Omega) = 1 and

       A3: for z be finite Subset of Omega holds (P . z) = ( setopfunc (z,Omega, REAL ,f, addreal ));

      

       A4: for A,B be Event of ( Trivial-SigmaField Omega) st A misses B holds (P . (A \/ B)) = ((P . A) + (P . B) qua Real)

      proof

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

        assume

         A5: A misses B;

        reconsider A0 = A, B0 = B as finite Subset of Omega;

        

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

        

        thus (P . (A \/ B)) = ( setopfunc ((A0 \/ B0),Omega, REAL ,f, addreal )) by A3

        .= ( addreal . (( setopfunc (A0,Omega, REAL ,f, addreal )),( setopfunc (B0,Omega, REAL ,f, addreal )))) by A5, A6, BHSP_5: 14

        .= ( addreal . (( setopfunc (A0,Omega, REAL ,f, addreal )),(P . B))) by A3

        .= ( addreal . ((P . A),(P . B))) by A3

        .= ((P . A) + (P . B) qua Real) by BINOP_2:def 9;

      end;

      

       A7: for A be Event of ( Trivial-SigmaField Omega) holds 0 <= (P . A) by A1;

      for ASeq be SetSequence of ( Trivial-SigmaField Omega) st ASeq is non-ascending holds (P * ASeq) is convergent & ( lim (P * ASeq)) = (P . ( Intersection ASeq))

      proof

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

        assume ASeq is non-ascending;

        then

        consider N be Nat such that

         A8: for m be Nat st N <= m holds ( Intersection ASeq) = (ASeq . m) by RANDOM_1: 15;

        now

          let m be Nat;

          assume

           A9: N <= m;

          m in NAT by ORDINAL1:def 12;

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

          

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

          .= (P . ( Intersection ASeq)) by A8, A9;

        end;

        hence thesis by PROB_1: 1;

      end;

      hence thesis by A7, A4, A2, PROB_1:def 8;

    end;

    

     Lm1: for Omega1,Omega2 be non empty finite set, P1 be Probability of ( Trivial-SigmaField Omega1), P2 be Probability of ( Trivial-SigmaField Omega2) holds ex Q be Function of [:Omega1, Omega2:], REAL st for x,y be set st x in Omega1 & y in Omega2 holds (Q . (x,y)) = ((P1 . {x}) * (P2 . {y}))

    proof

      let Omega1,Omega2 be non empty finite set, P1 be Probability of ( Trivial-SigmaField Omega1), P2 be Probability of ( Trivial-SigmaField Omega2);

      deffunc Q0( object, object) = ((P1 . {$1}) * (P2 . {$2}));

      consider f be Function such that

       A1: ( dom f) = [:Omega1, Omega2:] & for x,y be object st x in Omega1 & y in Omega2 holds (f . (x,y)) = Q0(x,y) from FUNCT_3:sch 2;

      for z be object st z in [:Omega1, Omega2:] holds (f . z) in REAL

      proof

        let z be object;

        assume z in [:Omega1, Omega2:];

        then

        consider x,y be object such that

         A2: x in Omega1 & y in Omega2 & z = [x, y] by ZFMISC_1:def 2;

        (f . z) = (f . (x,y)) by A2

        .= Q0(x,y) by A1, A2;

        hence (f . z) in REAL by XREAL_0:def 1;

      end;

      then

      reconsider f as Function of [:Omega1, Omega2:], REAL by A1, FUNCT_2: 3;

      take f;

      thus thesis by A1;

    end;

    

     Lm2: for Omega1,Omega2 be non empty finite set, P1 be Probability of ( Trivial-SigmaField Omega1), P2 be Probability of ( Trivial-SigmaField Omega2), Q1,Q2 be Function of [:Omega1, Omega2:], REAL st (for x,y be set st x in Omega1 & y in Omega2 holds (Q1 . (x,y)) = ((P1 . {x}) * (P2 . {y}))) & (for x,y be set st x in Omega1 & y in Omega2 holds (Q2 . (x,y)) = ((P1 . {x}) * (P2 . {y}))) holds Q1 = Q2

    proof

      let Omega1,Omega2 be non empty finite set, P1 be Probability of ( Trivial-SigmaField Omega1), P2 be Probability of ( Trivial-SigmaField Omega2), Q1,Q2 be Function of [:Omega1, Omega2:], REAL ;

      assume

       A1: (for x,y be set st x in Omega1 & y in Omega2 holds (Q1 . (x,y)) = ((P1 . {x}) * (P2 . {y}))) & (for x,y be set st x in Omega1 & y in Omega2 holds (Q2 . (x,y)) = ((P1 . {x}) * (P2 . {y})));

      

       A2: ( dom Q1) = [:Omega1, Omega2:] & ( dom Q2) = [:Omega1, Omega2:] by FUNCT_2:def 1;

      now

        let z be object;

        assume z in ( dom Q1);

        then

        consider x,y be object such that

         A3: x in Omega1 & y in Omega2 & z = [x, y] by ZFMISC_1:def 2;

        

        thus (Q1 . z) = (Q1 . (x,y)) by A3

        .= ((P1 . {x}) * (P2 . {y})) by A3, A1

        .= (Q2 . (x,y)) by A3, A1

        .= (Q2 . z) by A3;

      end;

      hence thesis by A2, FUNCT_1: 2;

    end;

    

     Lm3: for Omega1,Omega2 be non empty finite set, P1 be Probability of ( Trivial-SigmaField Omega1), P2 be Probability of ( Trivial-SigmaField Omega2), Q be Function of [:Omega1, Omega2:], REAL holds ex P be Function of ( bool [:Omega1, Omega2:]), REAL st for z be finite Subset of [:Omega1, Omega2:] holds (P . z) = ( setopfunc (z, [:Omega1, Omega2:], REAL ,Q, addreal ))

    proof

      let Omega1,Omega2 be non empty finite set, P1 be Probability of ( Trivial-SigmaField Omega1), P2 be Probability of ( Trivial-SigmaField Omega2), Q be Function of [:Omega1, Omega2:], REAL ;

      defpred PF[ object, object] means ex z be finite Subset of [:Omega1, Omega2:] st $1 = z & $2 = ( setopfunc (z, [:Omega1, Omega2:], REAL ,Q, addreal ));

      

       A1: for x be object st x in ( bool [:Omega1, Omega2:]) holds ex y be object st y in REAL & PF[x, y]

      proof

        let x be object;

        assume x in ( bool [:Omega1, Omega2:]);

        then

        reconsider z = x as finite Subset of [:Omega1, Omega2:];

        ( setopfunc (z, [:Omega1, Omega2:], REAL ,Q, addreal )) in REAL ;

        hence thesis;

      end;

      consider P be Function of ( bool [:Omega1, Omega2:]), REAL such that

       A2: for x be object st x in ( bool [:Omega1, Omega2:]) holds PF[x, (P . x)] from FUNCT_2:sch 1( A1);

      take P;

      thus for z be finite Subset of [:Omega1, Omega2:] holds (P . z) = ( setopfunc (z, [:Omega1, Omega2:], REAL ,Q, addreal ))

      proof

        let z be finite Subset of [:Omega1, Omega2:];

        ex z1 be finite Subset of [:Omega1, Omega2:] st z = z1 & (P . z) = ( setopfunc (z1, [:Omega1, Omega2:], REAL ,Q, addreal )) by A2;

        hence (P . z) = ( setopfunc (z, [:Omega1, Omega2:], REAL ,Q, addreal ));

      end;

    end;

    

     Lm4: for Omega1,Omega2 be non empty finite set, P1 be Probability of ( Trivial-SigmaField Omega1), P2 be Probability of ( Trivial-SigmaField Omega2), Q be Function of [:Omega1, Omega2:], REAL holds for P1,P2 be Function of ( bool [:Omega1, Omega2:]), REAL st (for z be finite Subset of [:Omega1, Omega2:] holds (P1 . z) = ( setopfunc (z, [:Omega1, Omega2:], REAL ,Q, addreal ))) & (for z be finite Subset of [:Omega1, Omega2:] holds (P2 . z) = ( setopfunc (z, [:Omega1, Omega2:], REAL ,Q, addreal ))) holds P1 = P2

    proof

      let Omega1,Omega2 be non empty finite set, P1 be Probability of ( Trivial-SigmaField Omega1), P2 be Probability of ( Trivial-SigmaField Omega2), Q be Function of [:Omega1, Omega2:], REAL ;

      let P1,P2 be Function of ( bool [:Omega1, Omega2:]), REAL ;

      assume

       A1: for z be finite Subset of [:Omega1, Omega2:] holds (P1 . z) = ( setopfunc (z, [:Omega1, Omega2:], REAL ,Q, addreal ));

      assume

       A2: for z be finite Subset of [:Omega1, Omega2:] holds (P2 . z) = ( setopfunc (z, [:Omega1, Omega2:], REAL ,Q, addreal ));

      now

        let x be object;

        assume x in ( bool [:Omega1, Omega2:]);

        then

        reconsider z = x as finite Subset of [:Omega1, Omega2:];

        

        thus (P1 . x) = ( setopfunc (z, [:Omega1, Omega2:], REAL ,Q, addreal )) by A1

        .= (P2 . x) by A2;

      end;

      hence P1 = P2 by FUNCT_2: 12;

    end;

    

     Lm5: for DK,DX be non empty set, F be Function of DX, DK, p,q be FinSequence of DX, fp,fq be FinSequence of DK st fp = (F * p) & fq = (F * q) holds (F * (p ^ q)) = (fp ^ fq)

    proof

      let DK,DX be non empty set, F be Function of DX, DK, p,q be FinSequence of DX, fp,fq be FinSequence of DK;

      assume

       A1: fp = (F * p) & fq = (F * q);

      then

       A2: ( dom fp) = ( dom p) & ( dom fq) = ( dom q) by FINSEQ_3: 120;

      

       A3: ( len fp) = ( len p) & ( len fq) = ( len q) by A1, FINSEQ_3: 120;

      then

       A4: ( dom (fp ^ fq)) = ( Seg (( len p) + ( len q))) by FINSEQ_1:def 7;

      

       A5: ( dom (F * (p ^ q))) = ( dom (p ^ q)) by FINSEQ_3: 120

      .= ( Seg (( len p) + ( len q))) by FINSEQ_1:def 7;

      for x be object st x in ( dom (F * (p ^ q))) holds ((fp ^ fq) . x) = ((F * (p ^ q)) . x)

      proof

        let x be object;

        assume

         A6: x in ( dom (F * (p ^ q)));

        then

        reconsider n = x as Element of NAT ;

        

         A7: 1 <= n & n <= (( len p) + ( len q)) by A6, A5, FINSEQ_1: 1;

        

         A8: ((F * (p ^ q)) . n) = (F . ((p ^ q) . n)) by A6, FINSEQ_3: 120;

        per cases ;

          suppose n <= ( len p);

          then n in ( Seg ( len p)) by A7;

          then

           A9: n in ( dom p) by FINSEQ_1:def 3;

          

          hence ((F * (p ^ q)) . x) = (F . (p . n)) by A8, FINSEQ_1:def 7

          .= (fp . n) by A1, A9, A2, FINSEQ_3: 120

          .= ((fp ^ fq) . x) by A9, A2, FINSEQ_1:def 7;

        end;

          suppose

           A10: not n <= ( len p);

          then ( len p) < n & n <= ( len (p ^ q)) by A7, FINSEQ_1: 22;

          then

           A11: ((p ^ q) . n) = (q . (n - ( len p))) by FINSEQ_1: 24;

          

           A12: (n - ( len p)) <= ((( len p) + ( len q)) - ( len p)) by A7, XREAL_1: 9;

          

           A13: (( len p) - ( len p)) < (n - ( len p)) by A10, XREAL_1: 9;

          

           A14: (n - ( len p)) is Element of NAT by A13, INT_1: 3;

          then 1 <= (n - ( len p)) by A13, NAT_1: 14;

          then (n - ( len p)) in ( Seg ( len q)) by A12, A14;

          then

           A15: (n - ( len p)) in ( dom q) by FINSEQ_1:def 3;

          

           A16: ( len fp) < n & n <= ( len (fp ^ fq)) by A3, A10, A7, FINSEQ_1: 22;

          

          thus ((F * (p ^ q)) . x) = (fq . (n - ( len p))) by A1, A15, A2, A11, A8, FINSEQ_3: 120

          .= ((fp ^ fq) . x) by A16, A3, FINSEQ_1: 24;

        end;

      end;

      hence thesis by A4, A5, FUNCT_1: 2;

    end;

    theorem :: RANDOM_2:9

    

     Th9: for DX be non empty set, F be Function of DX, REAL , Y be finite Subset of DX holds ex p be FinSequence of DX st p is one-to-one & ( rng p) = Y & ( setopfunc (Y,DX, REAL ,F, addreal )) = ( Sum ( Func_Seq (F,p)))

    proof

      let DX be non empty set, F be Function of DX, REAL , Y be finite Subset of DX;

      consider p be FinSequence of DX such that

       A1: p is one-to-one & ( rng p) = Y & ( setopfunc (Y,DX, REAL ,F, addreal )) = ( addreal "**" ( Func_Seq (F,p))) by BHSP_5:def 5;

      ( Sum ( Func_Seq (F,p))) = ( addreal "**" ( Func_Seq (F,p)));

      hence thesis by A1;

    end;

    theorem :: RANDOM_2:10

    

     Th10: for DX be non empty set, F be Function of DX, REAL , Y be finite Subset of DX, p be FinSequence of DX st p is one-to-one & ( rng p) = Y holds ( setopfunc (Y,DX, REAL ,F, addreal )) = ( Sum ( Func_Seq (F,p))) by BHSP_5:def 5;

    

     Lm6: for p be Function st ( dom p) = ( Seg 1) holds p = <*(p . 1)*>

    proof

      let p be Function;

      assume

       A1: ( dom p) = ( Seg 1);

      then

       A3: ( rng p) = {(p . 1)} by FINSEQ_1: 2, FUNCT_1: 4;

      p is FinSequence-like by A1;

      hence thesis by A3, A1, FINSEQ_1: 38;

    end;

    theorem :: RANDOM_2:11

    

     Th11: for DX1,DX2 be non empty set, F1 be Function of DX1, REAL , F2 be Function of DX2, REAL , G be Function of [:DX1, DX2:], REAL , Y1 be non empty finite Subset of DX1 holds for p1 be FinSequence of DX1 st p1 is one-to-one & ( rng p1) = Y1 holds for p2 be FinSequence of DX2, p3 be FinSequence of [:DX1, DX2:], Y2 be non empty finite Subset of DX2, Y3 be finite Subset of [:DX1, DX2:] st p2 is one-to-one & ( rng p2) = Y2 & p3 is one-to-one & ( rng p3) = Y3 & Y3 = [:Y1, Y2:] & for x,y be set st x in Y1 & y in Y2 holds (G . (x,y)) = ((F1 . x) * (F2 . y)) holds ( Sum ( Func_Seq (G,p3))) = (( Sum ( Func_Seq (F1,p1))) * ( Sum ( Func_Seq (F2,p2))))

    proof

      let DX1,DX2 be non empty set, F1 be Function of DX1, REAL , F2 be Function of DX2, REAL , G be Function of [:DX1, DX2:], REAL , Y1 be non empty finite Subset of DX1;

      let p1 be FinSequence of DX1;

      assume

       A1: p1 is one-to-one & ( rng p1) = Y1;

      defpred F[ Nat] means for p2 be FinSequence of DX2, p3 be FinSequence of [:DX1, DX2:], Y2 be non empty finite Subset of DX2, Y3 be finite Subset of [:DX1, DX2:] st ( len p2) = $1 & p2 is one-to-one & ( rng p2) = Y2 & p3 is one-to-one & ( rng p3) = Y3 & Y3 = [:Y1, Y2:] & for x,y be set st x in Y1 & y in Y2 holds (G . (x,y)) = ((F1 . x) * (F2 . y)) holds ( Sum ( Func_Seq (G,p3))) = (( Sum ( Func_Seq (F1,p1))) * ( Sum ( Func_Seq (F2,p2))));

      consider erp1 be object such that

       A2: erp1 in ( rng p1) by A1, XBOOLE_0:def 1;

      

       A3: ex x be object st x in ( dom p1) & erp1 = (p1 . x) by A2, FUNCT_1:def 3;

      

       A4: F[ 0 ]

      proof

        let p2 be FinSequence of DX2, p3 be FinSequence of [:DX1, DX2:], Y2 be non empty finite Subset of DX2, Y3 be finite Subset of [:DX1, DX2:];

        assume

         A5: ( len p2) = 0 & p2 is one-to-one & ( rng p2) = Y2 & p3 is one-to-one & ( rng p3) = Y3 & Y3 = [:Y1, Y2:] & for x,y be set st x in Y1 & y in Y2 holds (G . (x,y)) = ((F1 . x) * (F2 . y));

        then p2 = {} ;

        hence ( Sum ( Func_Seq (G,p3))) = (( Sum ( Func_Seq (F1,p1))) * ( Sum ( Func_Seq (F2,p2)))) by A5;

      end;

      

       A6: F[1]

      proof

        let p2 be FinSequence of DX2, p3 be FinSequence of [:DX1, DX2:], Y2 be non empty finite Subset of DX2, Y3 be finite Subset of [:DX1, DX2:];

        assume

         A7: ( len p2) = 1 & p2 is one-to-one & ( rng p2) = Y2 & p3 is one-to-one & ( rng p3) = Y3 & Y3 = [:Y1, Y2:] & for x,y be set st x in Y1 & y in Y2 holds (G . (x,y)) = ((F1 . x) * (F2 . y));

        then

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

        then

         A9: Y2 = {(p2 . 1)} by A7, FINSEQ_1: 38;

        set w = (p2 . 1);

        set z = ((F2 * p2) . 1);

        ( dom F2) = DX2 by FUNCT_2:def 1;

        then ( rng p2) c= ( dom F2);

        then ( dom (F2 * p2)) = ( dom p2) by RELAT_1: 27;

        then

         A10: ( dom (F2 * p2)) = ( Seg 1) by A8, FINSEQ_1: 38;

        then ( Func_Seq (F2,p2)) = <*z*> by Lm6;

        then

         A11: ( Sum ( Func_Seq (F2,p2))) = z by RVSUM_1: 73;

        

         A12: Y3 = [:Y1, {w}:] by A7, A8, FINSEQ_1: 38;

        

         A13: ( len p1) = ( card Y1) by A1, FINSEQ_4: 62;

        

         A14: ( len p3) = ( card ( rng p3)) by A7, FINSEQ_4: 62

        .= ( card Y1) by A12, A7, CARD_1: 69;

        

         A15: ( dom p1) = ( Seg ( card Y1)) by A13, FINSEQ_1:def 3

        .= ( dom p3) by A14, FINSEQ_1:def 3;

        deffunc Q33F( Nat) = [(p1 . $1), w];

        consider q3 be FinSequence such that

         A16: ( len q3) = ( len p3) and

         A17: for k be Nat st k in ( dom q3) holds (q3 . k) = Q33F(k) from FINSEQ_1:sch 2;

        

         A18: ( dom q3) = ( Seg ( len p3)) by A16, FINSEQ_1:def 3;

        

         A19: ( dom p3) = ( Seg ( len p3)) by FINSEQ_1:def 3;

        now

          let k be Nat;

          assume

           A20: k in ( dom q3);

          then

           A21: (p1 . k) in Y1 by A1, A18, A19, A15, FUNCT_1: 3;

          (p2 . 1) in Y2 by A9, TARSKI:def 1;

          then [(p1 . k), w] in [:Y1, Y2:] by A21, ZFMISC_1: 87;

          hence (q3 . k) in [:Y1, Y2:] by A20, A17;

        end;

        then q3 is FinSequence of [:Y1, Y2:] by FINSEQ_2: 12;

        then

         A22: ( rng q3) c= [:Y1, Y2:] by FINSEQ_1:def 4;

         [:Y1, Y2:] c= [:DX1, DX2:] by ZFMISC_1: 96;

        then ( rng q3) c= [:DX1, DX2:] by A22;

        then

        reconsider q3 as FinSequence of [:DX1, DX2:] by FINSEQ_1:def 4;

        now

          let x1,x2 be object;

          assume

           A23: x1 in ( dom q3) & x2 in ( dom q3) & (q3 . x1) = (q3 . x2);

          then

           A24: x1 in ( dom p1) & x2 in ( dom p1) by A16, A19, A15, FINSEQ_1:def 3;

          reconsider n1 = x1, n2 = x2 as Element of NAT by A23;

           [(p1 . n1), w] = (q3 . n1) by A17, A23

          .= [(p1 . n2), w] by A17, A23;

          then (p1 . n1) = (p1 . n2) by XTUPLE_0: 1;

          hence x1 = x2 by A1, A24, FUNCT_1:def 4;

        end;

        then

         A25: q3 is one-to-one by FUNCT_1:def 4;

        

         A26: ( rng q3) = [:Y1, Y2:]

        proof

          now

            let z be object;

            assume z in [:Y1, Y2:];

            then

            consider y1,y2 be object such that

             A27: y1 in Y1 & y2 in Y2 & z = [y1, y2] by ZFMISC_1:def 2;

            consider n1 be object such that

             A28: n1 in ( dom p1) & y1 = (p1 . n1) by A1, A27, FUNCT_1:def 3;

            reconsider n1 as Element of NAT by A28;

            

             A29: n1 in ( dom q3) by A28, A16, A19, A15, FINSEQ_1:def 3;

            y2 = w by A9, A27, TARSKI:def 1;

            then (q3 . n1) = z by A27, A28, A17, A29;

            hence z in ( rng q3) by A29, FUNCT_1: 3;

          end;

          then [:Y1, Y2:] c= ( rng q3);

          hence thesis by A22, XBOOLE_0:def 10;

        end;

        then

        consider P be Permutation of ( dom p3) such that

         A30: q3 = (p3 * P) & ( dom P) = ( dom p3) & ( rng P) = ( dom p3) by A25, A7, BHSP_5: 1;

        

         A31: ( Func_Seq (G,q3)) = (( Func_Seq (G,p3)) * P) by A30, RELAT_1: 36;

        ( dom G) = [:DX1, DX2:] by FUNCT_2:def 1;

        then ( rng p3) c= ( dom G);

        then ( dom ( Func_Seq (G,p3))) = ( dom p3) by RELAT_1: 27;

        then

         A32: ( Sum ( Func_Seq (G,q3))) = ( Sum ( Func_Seq (G,p3))) by A31, FINSOP_1: 7;

        

         A33: ( dom G) = [:DX1, DX2:] by FUNCT_2:def 1;

        ( dom F1) = DX1 by FUNCT_2:def 1;

        

        then

         A34: ( dom (F1 * p1)) = ( dom p1) by A1, RELAT_1: 27

        .= ( Seg ( len p1)) by FINSEQ_1:def 3;

        

         A35: ( dom (G * q3)) = ( dom q3) by A33, A26, RELAT_1: 27

        .= ( Seg ( len p1)) by A13, A14, A16, FINSEQ_1:def 3;

        then

         A36: ( dom (G * q3)) = ( dom (z (#) (F1 * p1))) by A34, VALUED_1:def 5;

        now

          let x be object;

          assume

           A37: x in ( dom (G * q3));

          then

          reconsider nx = x as Element of NAT ;

          ( dom (G * q3)) = ( dom q3) by A33, A26, RELAT_1: 27

          .= ( Seg ( len q3)) by FINSEQ_1:def 3;

          then

           A38: nx in ( dom q3) by A37, FINSEQ_1:def 3;

          1 <= nx & nx <= ( len p1) by A37, A35, FINSEQ_1: 1;

          then

           A39: (p1 /. nx) = (p1 . nx) by FINSEQ_4: 15;

          

           A40: (q3 . nx) = [(p1 . nx), w] by A17, A38;

          

           A41: nx in ( dom p1) by A37, A35, FINSEQ_1:def 3;

          then

           A42: (q3 . nx) = [(p1 /. nx), w] by A40, PARTFUN1:def 6;

          (p1 . nx) in Y1 by A41, A1, FUNCT_1: 3;

          then

           A43: (p1 /. nx) in Y1 & w in Y2 by A41, A9, PARTFUN1:def 6, TARSKI:def 1;

          1 in ( dom (F2 * p2)) by A10;

          then

           A44: z = (F2 . w) by FUNCT_1: 12;

          

          thus ((G * q3) . x) = (G . ((p1 /. nx),w)) by A42, A37, FUNCT_1: 12

          .= ((F1 . (p1 /. nx)) * z) by A44, A7, A43

          .= (((F1 * p1) . nx) * z) by A39, A35, A34, A37, FUNCT_1: 12

          .= ((z (#) (F1 * p1)) . x) by VALUED_1: 6;

        end;

        then ( Func_Seq (G,q3)) = (z * ( Func_Seq (F1,p1))) by A36, FUNCT_1: 2;

        hence thesis by A11, A32, RVSUM_1: 87;

      end;

      

       A45: for n be Nat st F[n] holds F[(n + 1)]

      proof

        let n be Nat;

        assume

         A46: F[n];

        now

          per cases ;

            case n = 0 ;

            hence F[(n + 1)] by A6;

          end;

            case

             A47: n > 0 ;

            now

              let p2 be FinSequence of DX2, p3 be FinSequence of [:DX1, DX2:], Y2 be non empty finite Subset of DX2, Y3 be finite Subset of [:DX1, DX2:];

              assume

               A48: ( len p2) = (n + 1) & p2 is one-to-one & ( rng p2) = Y2 & p3 is one-to-one & ( rng p3) = Y3 & Y3 = [:Y1, Y2:] & for x,y be set st x in Y1 & y in Y2 holds (G . (x,y)) = ((F1 . x) * (F2 . y));

              set lb = ( len p1);

              set la = ( len p2);

              deffunc FG1( Nat) = [(p1 . ((($1 -' 1) mod lb) + 1)), (p2 . ((($1 -' 1) div lb) + 1))];

              consider FG be FinSequence such that

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

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

              

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

              

               A52: ( dom p1) = ( Seg lb) by FINSEQ_1:def 3;

               A53:

              now

                reconsider lap = la, lbp = lb as Nat;

                let k be Nat;

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

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

                assume k in ( dom FG);

                then

                 A54: k in ( Seg (la * lb)) by A49, FINSEQ_1:def 3;

                then

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

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

                then

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

                1 <= k by A54, FINSEQ_1: 1;

                then

                 A57: lbp divides (lap * lbp) & 1 <= (la * lb) by A55, NAT_D:def 3, XXREAL_0: 2;

                

                 A58: lb <> 0 by A54;

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

                then (((lap * lbp) -' 1) div lbp) = (((lap * lbp) div lbp) - 1) by A57, NAT_2: 15;

                then

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

                reconsider la, lb as Nat;

                i >= ( 0 qua Nat + 1) & i <= la by A58, A59, NAT_D: 18, XREAL_1: 6;

                then i in ( Seg la);

                hence i in ( dom p2) by FINSEQ_1:def 3;

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

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

                then j in ( Seg lb);

                hence j in ( dom p1) by FINSEQ_1:def 3;

              end;

              now

                let k be Nat;

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

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

                assume

                 A60: k in ( dom FG);

                then

                 A61: (p2 . i) in ( rng p2) by A53, FUNCT_1: 3;

                (p1 . j) in ( rng p1) by A53, A60, FUNCT_1: 3;

                then [(p1 . j), (p2 . i)] in [:DX1, DX2:] by A61, ZFMISC_1: 87;

                hence (FG . k) in [:DX1, DX2:] by A50, A60;

              end;

              then

              reconsider q3 = FG as FinSequence of [:DX1, DX2:] by FINSEQ_2: 12;

              

               A62: ( len p1) = ( card Y1) by A1, FINSEQ_4: 62;

              now

                let x1,x2 be object;

                assume

                 A63: x1 in ( dom q3) & x2 in ( dom q3) & (q3 . x1) = (q3 . x2);

                then

                 A64: x1 in ( Seg ( len q3)) & x2 in ( Seg ( len q3)) by FINSEQ_1:def 3;

                reconsider n1 = x1, n2 = x2 as Element of NAT by A63;

                

                 A65: (q3 . n1) = [(p1 . (((n1 -' 1) mod lb) + 1)), (p2 . (((n1 -' 1) div lb) + 1))] by A50, A63;

                

                 A66: (q3 . n2) = [(p1 . (((n2 -' 1) mod lb) + 1)), (p2 . (((n2 -' 1) div lb) + 1))] by A50, A63;

                then

                 A67: (p1 . (((n1 -' 1) mod lb) + 1)) = (p1 . (((n2 -' 1) mod lb) + 1)) by A63, A65, XTUPLE_0: 1;

                (((n1 -' 1) mod lb) + 1) in ( dom p1) & (((n2 -' 1) mod lb) + 1) in ( dom p1) by A63, A53;

                then

                 A68: (((n1 -' 1) mod lb) + 1) = (((n2 -' 1) mod lb) + 1) by A1, A67, FUNCT_1:def 4;

                

                 A69: (p2 . (((n1 -' 1) div lb) + 1)) = (p2 . (((n2 -' 1) div lb) + 1)) by A63, A65, A66, XTUPLE_0: 1;

                (((n1 -' 1) div lb) + 1) in ( dom p2) & (((n2 -' 1) div lb) + 1) in ( dom p2) by A63, A53;

                then

                 A70: (((n1 -' 1) div lb) + 1) = (((n2 -' 1) div lb) + 1) by A48, A69, FUNCT_1:def 4;

                n1 = n2

                proof

                  

                   A71: 1 <= n1 & n1 <= ( len q3) by A64, FINSEQ_1: 1;

                  

                   A72: 1 <= n2 & n2 <= ( len q3) by A64, FINSEQ_1: 1;

                   0 < lb by A52, A3;

                  then

                   A73: (n1 -' 1) = ((lb * ((n1 -' 1) div lb)) + ((n1 -' 1) mod lb)) & (n2 -' 1) = ((lb * ((n1 -' 1) div lb)) + ((n1 -' 1) mod lb)) by A68, A70, NAT_D: 2;

                  

                   A74: ((n1 -' 1) + 1) = ((n1 + 1) -' 1) by A71, NAT_D: 38

                  .= n1 by NAT_D: 34;

                  ((n2 -' 1) + 1) = ((n2 + 1) -' 1) by A72, NAT_D: 38

                  .= n2 by NAT_D: 34;

                  hence thesis by A73, A74;

                end;

                hence x1 = x2;

              end;

              then

               A75: q3 is one-to-one by FUNCT_1:def 4;

              

               A76: ( rng q3) = [:Y1, Y2:]

              proof

                now

                  let z be object;

                  assume z in [:Y1, Y2:];

                  then

                  consider y1,y2 be object such that

                   A77: y1 in Y1 & y2 in Y2 & z = [y1, y2] by ZFMISC_1:def 2;

                  consider n1 be object such that

                   A78: n1 in ( dom p1) & y1 = (p1 . n1) by A1, A77, FUNCT_1:def 3;

                  

                   A79: n1 in ( Seg ( len p1)) by A78, FINSEQ_1:def 3;

                  reconsider n1 as Element of NAT by A78;

                  consider n2 be object such that

                   A80: n2 in ( dom p2) & y2 = (p2 . n2) by A48, A77, FUNCT_1:def 3;

                  

                   A81: n2 in ( Seg ( len p2)) by A80, FINSEQ_1:def 3;

                  reconsider n2 as Element of NAT by A80;

                  

                   A82: 1 <= n1 & n1 <= ( len p1) by A79, FINSEQ_1: 1;

                  

                   A83: 1 <= n2 & n2 <= ( len p2) by A81, FINSEQ_1: 1;

                  reconsider n11 = (n1 - 1) as Element of NAT by A82, INT_1: 5;

                  reconsider n21 = (n2 - 1) as Element of NAT by A83, INT_1: 5;

                  set k1 = (n11 + (lb * n21));

                  

                   A84: n11 <= (( len p1) - 1) by A82, XREAL_1: 9;

                  (( len p1) - 1) < ( len p1) by XREAL_1: 44;

                  then

                   A85: n11 < ( len p1) by A84, XXREAL_0: 2;

                  

                   A86: (k1 div lb) = ((n11 div lb) + n21) by A62, NAT_D: 61

                  .= ( 0 qua Nat + n21) by A85, NAT_D: 27

                  .= n21;

                  

                   A87: (k1 mod lb) = (n11 mod lb) by NAT_D: 61

                  .= n11 by A85, NAT_D: 24;

                  set k = (k1 + 1);

                  

                   A88: 1 <= k by NAT_1: 14;

                  

                   A89: (k -' 1) = (k - 1) by NAT_1: 14, XREAL_1: 233

                  .= k1;

                  then

                   A90: n1 = (((k -' 1) mod lb) + 1) by A87;

                  

                   A91: n2 = (((k -' 1) div lb) + 1) by A89, A86;

                  

                   A92: ((n11 + 1) + (lb * n21)) <= (( len p1) + (lb * n21)) by A82, XREAL_1: 6;

                  n21 <= (( len p2) - 1) by A83, XREAL_1: 9;

                  then (lb * n21) <= (lb * (( len p2) - 1)) by XREAL_1: 64;

                  then (( len p1) + (lb * n21)) <= (( len p1) + (lb * (( len p2) - 1))) by XREAL_1: 6;

                  then k <= (lb * la) by A92, XXREAL_0: 2;

                  then k in ( Seg ( len FG)) by A49, A88;

                  then

                   A93: k in ( dom FG) by FINSEQ_1:def 3;

                  then (q3 . k) = z by A77, A78, A80, A50, A90, A91;

                  hence z in ( rng q3) by A93, FUNCT_1: 3;

                end;

                then

                 A94: [:Y1, Y2:] c= ( rng q3);

                now

                  let z be object;

                  assume z in ( rng q3);

                  then

                  consider n1 be object such that

                   A95: n1 in ( dom q3) & z = (q3 . n1) by FUNCT_1:def 3;

                  reconsider n1 as Element of NAT by A95;

                  

                   A96: z = [(p1 . (((n1 -' 1) mod lb) + 1)), (p2 . (((n1 -' 1) div lb) + 1))] by A95, A50;

                  

                   A97: (p1 . (((n1 -' 1) mod lb) + 1)) in Y1 by A1, A95, A53, FUNCT_1: 3;

                  (((n1 -' 1) div lb) + 1) in ( dom p2) by A95, A53;

                  then (p2 . (((n1 -' 1) div lb) + 1)) in Y2 by A48, FUNCT_1: 3;

                  hence z in [:Y1, Y2:] by A96, A97, ZFMISC_1:def 2;

                end;

                then ( rng q3) c= [:Y1, Y2:];

                hence thesis by A94, XBOOLE_0:def 10;

              end;

              set q30 = (q3 | (lb * n));

              (lb * n) <= (lb * la) by A48, NAT_1: 11, XREAL_1: 64;

              then

               A98: ( len q30) = (lb * n) by A49, FINSEQ_1: 17;

              set q31 = (q3 /^ (lb * n));

              reconsider q30 as FinSequence of [:DX1, DX2:];

              reconsider q31 as FinSequence of [:DX1, DX2:];

              

               A99: q3 = (q30 ^ q31) by RFINSEQ: 8;

              set p20 = (p2 | n);

              reconsider p20 as FinSequence of DX2;

              

               A100: ( len p20) = n by A48, FINSEQ_3: 53;

              then

               A101: ( dom p20) is non empty by A47, FINSEQ_1:def 3;

              

               A102: p20 is one-to-one by A48, FUNCT_1: 52;

              reconsider Y20 = ( rng p20) as non empty finite Subset of DX2 by A101, RELAT_1: 42;

              

               A103: q30 is one-to-one by A75, FUNCT_1: 52;

              

               A104: ( rng q30) = [:Y1, Y20:]

              proof

                now

                  let z be object;

                  assume z in [:Y1, Y20:];

                  then

                  consider y1,y2 be object such that

                   A105: y1 in Y1 & y2 in Y20 & z = [y1, y2] by ZFMISC_1:def 2;

                  consider n1 be object such that

                   A106: n1 in ( dom p1) & y1 = (p1 . n1) by A1, A105, FUNCT_1:def 3;

                  

                   A107: n1 in ( Seg ( len p1)) by A106, FINSEQ_1:def 3;

                  reconsider n1 as Element of NAT by A106;

                  consider n2 be object such that

                   A108: n2 in ( dom p20) & y2 = (p20 . n2) by A105, FUNCT_1:def 3;

                  

                   A109: n2 in ( Seg ( len p20)) by A108, FINSEQ_1:def 3;

                  reconsider n2 as Element of NAT by A108;

                  

                   A110: y2 = (p2 . n2) by A108, FUNCT_1: 47;

                  

                   A111: 1 <= n1 & n1 <= ( len p1) by A107, FINSEQ_1: 1;

                  

                   A112: 1 <= n2 & n2 <= ( len p20) by A109, FINSEQ_1: 1;

                  reconsider n11 = (n1 - 1) as Element of NAT by A111, INT_1: 5;

                  reconsider n21 = (n2 - 1) as Element of NAT by A112, INT_1: 5;

                  set k1 = (n11 + (lb * n21));

                  

                   A113: n11 <= (( len p1) - 1) by A111, XREAL_1: 9;

                  (( len p1) - 1) < ( len p1) by XREAL_1: 44;

                  then

                   A114: n11 < ( len p1) by A113, XXREAL_0: 2;

                  

                   A115: (k1 div lb) = ((n11 div lb) + n21) by A62, NAT_D: 61

                  .= ( 0 qua Nat + n21) by A114, NAT_D: 27

                  .= n21;

                  

                   A116: (k1 mod lb) = (n11 mod lb) by NAT_D: 61

                  .= n11 by A114, NAT_D: 24;

                  set k = (k1 + 1);

                  

                   A117: 1 <= k by NAT_1: 14;

                  

                   A118: (k -' 1) = (k - 1) by NAT_1: 14, XREAL_1: 233

                  .= k1;

                  then

                   A119: n1 = (((k -' 1) mod lb) + 1) by A116;

                  

                   A120: n2 = (((k -' 1) div lb) + 1) by A118, A115;

                  

                   A121: ((n11 + 1) + (lb * n21)) <= (( len p1) + (lb * n21)) by A111, XREAL_1: 6;

                  n21 <= (( len p20) - 1) by A112, XREAL_1: 9;

                  then (lb * n21) <= (lb * (( len p20) - 1)) by XREAL_1: 64;

                  then (( len p1) + (lb * n21)) <= (( len p1) + (lb * (( len p20) - 1))) by XREAL_1: 6;

                  then k <= (lb * n) by A121, A100, XXREAL_0: 2;

                  then k in ( Seg ( len q30)) by A117, A98;

                  then

                   A122: k in ( dom q30) by FINSEQ_1:def 3;

                  then

                   A123: k in ( dom q3) by RELAT_1: 57;

                  (q30 . k) = (q3 . k) by A122, FUNCT_1: 47

                  .= z by A105, A106, A110, A50, A123, A119, A120;

                  hence z in ( rng q30) by A122, FUNCT_1: 3;

                end;

                then

                 A124: [:Y1, Y20:] c= ( rng q30);

                now

                  let z be object;

                  assume z in ( rng q30);

                  then

                  consider n1 be object such that

                   A125: n1 in ( dom q30) & z = (q30 . n1) by FUNCT_1:def 3;

                  

                   A126: n1 in ( Seg ( len q30)) by A125, FINSEQ_1:def 3;

                  reconsider n1 as Element of NAT by A125;

                  

                   A127: n1 in ( dom q3) by A125, RELAT_1: 57;

                  z = (q3 . n1) by A125, FUNCT_1: 47;

                  then

                   A128: z = [(p1 . (((n1 -' 1) mod lb) + 1)), (p2 . (((n1 -' 1) div lb) + 1))] by A50, A127;

                  

                   A129: (p1 . (((n1 -' 1) mod lb) + 1)) in Y1 by A1, A127, A53, FUNCT_1: 3;

                  

                   A130: 1 <= n1 & n1 <= (lb * n) by A126, A98, FINSEQ_1: 1;

                  

                   A131: lb divides (lb * n) by INT_1:def 3;

                  

                   A132: 1 <= lb by A62, NAT_1: 14;

                  1 <= (lb * n) by A62, A47, NAT_1: 14;

                  

                  then

                   A133: (((lb * n) -' 1) div lb) = (((lb * n) div lb) - 1) by A131, A132, NAT_2: 15

                  .= (n - 1) by A62, NAT_D: 18;

                  (n1 -' 1) <= ((lb * n) -' 1) by A130, NAT_D: 42;

                  then ((n1 -' 1) div lb) <= (((lb * n) -' 1) div lb) by NAT_2: 24;

                  then

                   A134: (((n1 -' 1) div lb) + 1) <= ((n - 1) + 1) by A133, XREAL_1: 6;

                  (((n1 -' 1) div lb) + 1) in ( dom p2) by A127, A53;

                  then (((n1 -' 1) div lb) + 1) in ( Seg ( len p2)) by FINSEQ_1:def 3;

                  then 1 <= (((n1 -' 1) div lb) + 1) & (((n1 -' 1) div lb) + 1) <= n by A134, FINSEQ_1: 1;

                  then

                   A135: (((n1 -' 1) div lb) + 1) in ( Seg n);

                  (((n1 -' 1) div lb) + 1) in ( dom p2) by A127, A53;

                  then

                   A136: (((n1 -' 1) div lb) + 1) in ( dom p20) by A135, RELAT_1: 57;

                  then (p20 . (((n1 -' 1) div lb) + 1)) in Y20 by FUNCT_1: 3;

                  then (p2 . (((n1 -' 1) div lb) + 1)) in Y20 by A136, FUNCT_1: 47;

                  hence z in [:Y1, Y20:] by A128, A129, ZFMISC_1:def 2;

                end;

                then ( rng q30) c= [:Y1, Y20:];

                hence thesis by A124, XBOOLE_0:def 10;

              end;

              now

                let x,y be set;

                assume

                 A137: x in Y1 & y in Y20;

                Y20 c= ( rng p2) by RELAT_1: 70;

                hence (G . (x,y)) = ((F1 . x) * (F2 . y)) by A48, A137;

              end;

              then

               A138: ( Sum ( Func_Seq (G,q30))) = (( Sum ( Func_Seq (F1,p1))) * ( Sum ( Func_Seq (F2,p20)))) by A46, A102, A103, A104, A100;

              ( dom F1) = DX1 by FUNCT_2:def 1;

              

              then

               A139: ( dom (F1 * p1)) = ( dom p1) by A1, RELAT_1: 27

              .= ( Seg ( len p1)) by FINSEQ_1:def 3;

              

               A140: ( dom G) = [:DX1, DX2:] by FUNCT_2:def 1;

              ( len q3) = ((n * lb) + lb) by A48, A49;

              then

               A141: (n * lb) <= ( len q3) by NAT_1: 11;

              

              then

               A142: ( len q31) = (( len q3) - (lb * n)) by RFINSEQ:def 1

              .= lb by A48, A49;

              

               A143: [:Y1, Y2:] c= [:DX1, DX2:] & ( rng q31) c= ( rng q3) by A48, FINSEQ_5: 33;

              

              then

               A144: ( dom (G * q31)) = ( dom q31) by A140, RELAT_1: 27

              .= ( Seg ( len p1)) by A142, FINSEQ_1:def 3;

              then

               A145: ( dom (G * q31)) = ( dom ((( Func_Seq (F2,p2)) /. (n + 1)) (#) (F1 * p1))) by A139, VALUED_1:def 5;

              now

                let x be object;

                assume

                 A146: x in ( dom (G * q31));

                then

                reconsider nx = x as Element of NAT ;

                

                 A147: ( dom (G * q31)) = ( dom q31) by A140, A143, RELAT_1: 27

                .= ( Seg ( len q31)) by FINSEQ_1:def 3;

                

                 A148: 1 <= nx & nx <= ( len p1) by A146, A144, FINSEQ_1: 1;

                then

                 A149: (p1 /. nx) = (p1 . nx) by FINSEQ_4: 15;

                

                 A150: 1 <= (n + 1) & (n + 1) <= ( len p2) by A48, XREAL_1: 31;

                then

                 A151: (n + 1) in ( Seg ( len p2));

                then

                 A152: (n + 1) in ( dom p2) by FINSEQ_1:def 3;

                

                 A153: (p2 /. (n + 1)) = (p2 . (n + 1)) by A150, FINSEQ_4: 15;

                ( dom F2) = DX2 by FUNCT_2:def 1;

                then ( rng p2) c= ( dom F2);

                then

                 A154: (n + 1) in ( dom (F2 * p2)) by A152, RELAT_1: 27;

                

                 A155: (F2 . (p2 /. (n + 1))) = ((F2 * p2) . (n + 1)) by A152, A153, FUNCT_1: 13

                .= (( Func_Seq (F2,p2)) /. (n + 1)) by A154, PARTFUN1:def 6;

                

                 A156: 1 <= nx & nx <= lb by A147, A146, A142, FINSEQ_1: 1;

                then

                 A157: (nx + (lb * n)) <= (lb + (lb * n)) by XREAL_1: 6;

                

                 A158: nx <= (nx + (lb * n)) by NAT_1: 11;

                then 1 <= (nx + (lb * n)) & (nx + (lb * n)) <= (lb * la) by A157, A48, A156, XXREAL_0: 2;

                then (nx + (lb * n)) in ( dom FG) by A51;

                then

                 A159: (q3 . (nx + (lb * n))) = [(p1 . ((((nx + (lb * n)) -' 1) mod lb) + 1)), (p2 . ((((nx + (lb * n)) -' 1) div lb) + 1))] by A50;

                

                 A160: nx in ( dom q31) by A147, A146, FINSEQ_1:def 3;

                

                 A161: ((nx + (lb * n)) -' 1) = ((nx + (lb * n)) - 1) by A158, A156, XREAL_1: 233, XXREAL_0: 2

                .= ((nx - 1) + (lb * n))

                .= ((nx -' 1) + (lb * n)) by A148, XREAL_1: 233;

                (nx - 1) < nx by XREAL_1: 44;

                then (nx - 1) < lb by A156, XXREAL_0: 2;

                then

                 A162: (nx -' 1) < lb by A148, XREAL_1: 233;

                

                 A163: ((((nx -' 1) + (lb * n)) div lb) + 1) = ((((nx -' 1) div lb) + n) + 1) by A62, NAT_D: 61

                .= (( 0 qua Nat + n) + 1) by A162, NAT_D: 27;

                

                 A164: ((((nx -' 1) + (lb * n)) mod lb) + 1) = (((nx -' 1) mod lb) + 1) by NAT_D: 61

                .= ((nx -' 1) + 1) by A162, NAT_D: 24

                .= ((nx - 1) + 1) by A148, XREAL_1: 233;

                

                 A165: nx in ( dom p1) & (n + 1) in ( dom p2) by A146, A144, A151, FINSEQ_1:def 3;

                then (p1 /. nx) = (p1 . nx) & (p2 . (n + 1)) = (p2 /. (n + 1)) by PARTFUN1:def 6;

                then

                 A166: (q31 . nx) = [(p1 /. nx), (p2 /. (n + 1))] by A160, A159, A141, A161, A163, A164, RFINSEQ:def 1;

                (p1 . nx) in Y1 & (p2 . (n + 1)) in Y2 by A165, A48, A1, FUNCT_1: 3;

                then

                 A167: (p1 /. nx) in Y1 & (p2 /. (n + 1)) in Y2 by A165, PARTFUN1:def 6;

                

                thus ((G * q31) . x) = (G . ((p1 /. nx),(p2 /. (n + 1)))) by A166, A146, FUNCT_1: 12

                .= ((F1 . (p1 /. nx)) * (F2 . (p2 /. (n + 1)))) by A48, A167

                .= (((F1 * p1) . nx) * (( Func_Seq (F2,p2)) /. (n + 1))) by A155, A149, A139, A146, A144, FUNCT_1: 12

                .= (((( Func_Seq (F2,p2)) /. (n + 1)) (#) (F1 * p1)) . x) by VALUED_1: 6;

              end;

              then ( Func_Seq (G,q31)) = ((( Func_Seq (F2,p2)) /. (n + 1)) * ( Func_Seq (F1,p1))) by A145, FUNCT_1: 2;

              then

               A168: ( Sum ( Func_Seq (G,q31))) = (( Sum ( Func_Seq (F1,p1))) * (( Func_Seq (F2,p2)) /. (n + 1))) by RVSUM_1: 87;

              

               A169: ( Func_Seq (G,q3)) = (( Func_Seq (G,q30)) ^ ( Func_Seq (G,q31))) by A99, Lm5;

              ( dom F2) = DX2 by FUNCT_2:def 1;

              then ( rng p2) c= ( dom F2);

              then ( dom (F2 * p2)) = ( dom p2) by RELAT_1: 27;

              then ( dom ( Func_Seq (F2,p2))) = ( Seg ( len p2)) by FINSEQ_1:def 3;

              then

               A170: ( len ( Func_Seq (F2,p2))) = (n + 1) by A48, FINSEQ_1:def 3;

              (( Func_Seq (F2,p2)) | n) = ( Func_Seq (F2,p20)) by RELAT_1: 83;

              then

               A171: ( Func_Seq (F2,p2)) = (( Func_Seq (F2,p20)) ^ <*(( Func_Seq (F2,p2)) /. (n + 1))*>) by A170, FINSEQ_5: 21;

              

               A172: ( Sum ( Func_Seq (G,q3))) = (( Sum ( Func_Seq (G,q30))) + ( Sum ( Func_Seq (G,q31)))) by A169, RVSUM_1: 75

              .= (( Sum ( Func_Seq (F1,p1))) * (( Sum ( Func_Seq (F2,p20))) + (( Func_Seq (F2,p2)) /. (n + 1)))) by A138, A168

              .= (( Sum ( Func_Seq (F1,p1))) * ( Sum ( Func_Seq (F2,p2)))) by A171, RVSUM_1: 74;

              consider P be Permutation of ( dom p3) such that

               A173: q3 = (p3 * P) & ( dom P) = ( dom p3) & ( rng P) = ( dom p3) by A75, A76, A48, BHSP_5: 1;

              

               A174: ( Func_Seq (G,q3)) = (( Func_Seq (G,p3)) * P) by A173, RELAT_1: 36;

              ( dom G) = [:DX1, DX2:] by FUNCT_2:def 1;

              then ( rng p3) c= ( dom G);

              then ( dom ( Func_Seq (G,p3))) = ( dom p3) by RELAT_1: 27;

              hence ( Sum ( Func_Seq (G,p3))) = (( Sum ( Func_Seq (F1,p1))) * ( Sum ( Func_Seq (F2,p2)))) by A172, A174, FINSOP_1: 7;

            end;

            hence F[(n + 1)];

          end;

        end;

        hence F[(n + 1)];

      end;

      

       A175: for n be Nat holds F[n] from NAT_1:sch 2( A4, A45);

      now

        let p2 be FinSequence of DX2, p3 be FinSequence of [:DX1, DX2:], Y2 be non empty finite Subset of DX2, Y3 be finite Subset of [:DX1, DX2:];

        assume

         A176: p2 is one-to-one & ( rng p2) = Y2 & p3 is one-to-one & ( rng p3) = Y3 & Y3 = [:Y1, Y2:] & for x,y be set st x in Y1 & y in Y2 holds (G . (x,y)) = ((F1 . x) * (F2 . y));

        ( len p2) is Element of NAT ;

        hence ( Sum ( Func_Seq (G,p3))) = (( Sum ( Func_Seq (F1,p1))) * ( Sum ( Func_Seq (F2,p2)))) by A175, A176;

      end;

      hence thesis;

    end;

    theorem :: RANDOM_2:12

    

     Th12: for DX1,DX2 be non empty set, F1 be Function of DX1, REAL , F2 be Function of DX2, REAL , G be Function of [:DX1, DX2:], REAL , Y1 be non empty finite Subset of DX1, Y2 be non empty finite Subset of DX2, Y3 be finite Subset of [:DX1, DX2:] st Y3 = [:Y1, Y2:] & for x,y be set st x in Y1 & y in Y2 holds (G . (x,y)) = ((F1 . x) * (F2 . y)) holds ( setopfunc (Y3, [:DX1, DX2:], REAL ,G, addreal )) = (( setopfunc (Y1,DX1, REAL ,F1, addreal )) * ( setopfunc (Y2,DX2, REAL ,F2, addreal )))

    proof

      let DX1,DX2 be non empty set, F1 be Function of DX1, REAL , F2 be Function of DX2, REAL , G be Function of [:DX1, DX2:], REAL , Y1 be non empty finite Subset of DX1, Y2 be non empty finite Subset of DX2, Y3 be finite Subset of [:DX1, DX2:];

      assume

       A1: Y3 = [:Y1, Y2:] & for x,y be set st x in Y1 & y in Y2 holds (G . (x,y)) = ((F1 . x) * (F2 . y));

      consider p1 be FinSequence of DX1 such that

       A2: p1 is one-to-one & ( rng p1) = Y1 & ( setopfunc (Y1,DX1, REAL ,F1, addreal )) = ( Sum ( Func_Seq (F1,p1))) by Th9;

      consider p2 be FinSequence of DX2 such that

       A3: p2 is one-to-one & ( rng p2) = Y2 & ( setopfunc (Y2,DX2, REAL ,F2, addreal )) = ( Sum ( Func_Seq (F2,p2))) by Th9;

      consider p3 be FinSequence of [:DX1, DX2:] such that

       A4: p3 is one-to-one & ( rng p3) = Y3 & ( setopfunc (Y3, [:DX1, DX2:], REAL ,G, addreal )) = ( Sum ( Func_Seq (G,p3))) by Th9;

      thus thesis by A1, A2, A3, A4, Th11;

    end;

    theorem :: RANDOM_2:13

    

     Th13: for DX be non empty set, F be Function of DX, REAL , Y be finite Subset of DX st for x be set st x in Y holds 0 <= (F . x) holds 0 <= ( setopfunc (Y,DX, REAL ,F, addreal ))

    proof

      let DX be non empty set, F be Function of DX, REAL , Y be finite Subset of DX;

      assume

       A1: for x be set st x in Y holds 0 <= (F . x);

      consider p be FinSequence of DX such that

       A2: p is one-to-one & ( rng p) = Y & ( setopfunc (Y,DX, REAL ,F, addreal )) = ( Sum ( Func_Seq (F,p))) by Th9;

      now

        let i be Nat;

        assume

         A3: i in ( dom ( Func_Seq (F,p)));

        then

         A4: (( Func_Seq (F,p)) . i) = (F . (p . i)) by FUNCT_1: 12;

        i in ( dom p) by A3, FUNCT_1: 11;

        hence 0 <= (( Func_Seq (F,p)) . i) by A4, A1, A2, FUNCT_1: 3;

      end;

      hence thesis by A2, RVSUM_1: 84;

    end;

    theorem :: RANDOM_2:14

    

     Th14: for DX be non empty set, F be Function of DX, REAL , Y1,Y2 be finite Subset of DX st Y1 c= Y2 & for x be set st x in Y2 holds 0 <= (F . x) holds ( setopfunc (Y1,DX, REAL ,F, addreal )) <= ( setopfunc (Y2,DX, REAL ,F, addreal ))

    proof

      let DX be non empty set, F be Function of DX, REAL , Y1,Y2 be finite Subset of DX;

      assume

       A1: Y1 c= Y2 & for x be set st x in Y2 holds 0 <= (F . x);

      consider p1 be FinSequence of DX such that

       A2: p1 is one-to-one & ( rng p1) = Y1 & ( setopfunc (Y1,DX, REAL ,F, addreal )) = ( Sum ( Func_Seq (F,p1))) by Th9;

      reconsider Y3 = (Y2 \ Y1) as finite Subset of DX;

      consider p2 be FinSequence of DX such that

       A3: p2 is one-to-one & ( rng p2) = Y3 & ( setopfunc (Y3,DX, REAL ,F, addreal )) = ( Sum ( Func_Seq (F,p2))) by Th9;

      now

        let i be Nat;

        assume

         A4: i in ( dom ( Func_Seq (F,p2)));

        then

         A5: (( Func_Seq (F,p2)) . i) = (F . (p2 . i)) by FUNCT_1: 12;

        i in ( dom p2) by A4, FUNCT_1: 11;

        then

         A6: (p2 . i) in Y3 by A3, FUNCT_1: 3;

        Y3 c= Y2 by XBOOLE_1: 36;

        hence 0 <= (( Func_Seq (F,p2)) . i) by A5, A1, A6;

      end;

      then

       A7: 0 <= ( Sum ( Func_Seq (F,p2))) by RVSUM_1: 84;

      reconsider p3 = (p1 ^ p2) as FinSequence of DX;

      

       A8: ( rng p3) = (( rng p1) \/ ( rng p2)) by FINSEQ_1: 31

      .= (Y1 \/ Y2) by A3, A2, XBOOLE_1: 39

      .= Y2 by A1, XBOOLE_1: 12;

      ( rng p1) misses ( rng p2) by A2, A3, XBOOLE_1: 79;

      then p3 is one-to-one by A2, A3, FINSEQ_3: 91;

      then

       A9: ( setopfunc (Y2,DX, REAL ,F, addreal )) = ( Sum ( Func_Seq (F,p3))) by A8, Th10;

      

       A10: ( Func_Seq (F,p3)) = (( Func_Seq (F,p1)) ^ ( Func_Seq (F,p2))) by Lm5;

      (( Sum ( Func_Seq (F,p1))) + 0 qua Real) <= (( Sum ( Func_Seq (F,p1))) + ( Sum ( Func_Seq (F,p2)))) by A7, XREAL_1: 6;

      hence thesis by A2, A10, A9, RVSUM_1: 75;

    end;

    theorem :: RANDOM_2:15

    

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

    proof

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

      set YN = (Omega \ Y);

      

       A1: ( dom (YN --> 0 )) = YN & ( rng (YN --> 0 )) c= REAL by FUNCOP_1: 13;

      

       A2: ( dom (f +* (YN --> 0 ))) = (( dom f) \/ ( dom (YN --> 0 ))) by FUNCT_4:def 1

      .= (Omega \/ YN) by A1, FUNCT_2:def 1

      .= Omega by XBOOLE_1: 12;

      ( rng (f +* (YN --> 0 ))) c= REAL ;

      then

      reconsider g = (f +* (YN --> 0 )) as Function of Omega, REAL by A2, FUNCT_2: 2;

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

       A3: ( 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) = ((g . (s . n)) * (P . {(s . n)}))) & ( Integral (( P2M P),g)) = ( Sum G) by RANDOM_1: 13;

      reconsider g as Real-Valued-Random-Variable of ( Trivial-SigmaField Omega) by RANDOM_1: 29;

      

       A4: ( dom g) = Omega by FUNCT_2:def 1;

      g is_integrable_on P by RANDOM_1: 30;

      then

       A5: g is_integrable_on ( P2M P) by RANDOM_1:def 3;

      

       A6: Y misses YN by XBOOLE_1: 79;

      

       A7: ( Integral (( P2M P),(g | (Y \/ YN)))) = (( Integral (( P2M P),(g | Y))) + ( Integral (( P2M P),(g | YN)))) by A5, MESFUNC6: 92, XBOOLE_1: 79;

      (Y \/ YN) = (Y \/ Omega) by XBOOLE_1: 39

      .= Omega by XBOOLE_1: 12;

      then

       A8: (g | (Y \/ YN)) = g;

      

       A9: (g | Y) = (f | Y) by A1, A6, FUNCT_4: 72;

      

       A10: ( dom (g | YN)) = YN by A4, RELAT_1: 62;

      reconsider zz = 0 as R_eal by XXREAL_0:def 1;

      

       A11: for x be object st x in ( dom (g | YN)) holds ((g | YN) . x) = 0

      proof

        let x be object;

        assume

         A12: x in ( dom (g | YN));

        then

         A13: x in YN & ((g | YN) . x) = (g . x) by A4, FUNCT_1: 47, RELAT_1: 62;

        (g . x) = ((YN --> 0 ) . x) by A12, A1, A10, FUNCT_4: 13;

        hence thesis by A13, FUNCOP_1: 7;

      end;

      

      then ( Integral (( P2M P),(g | YN))) = (zz * (( P2M P) . YN)) by A10, MESFUNC6: 97

      .= 0 ;

      then

       A14: ( Integral (( P2M P),g)) = ( Integral (( P2M P),(f | Y))) by A9, A7, A8, XXREAL_3: 4;

      set N1 = (s " Y);

      s is Function of ( dom s), ( rng s) by FUNCT_2: 1;

      then N1 is finite Subset of ( dom s) by FUNCT_2: 39;

      then

      reconsider N1 as finite Subset of ( Seg ( len G)) by A3, FINSEQ_1:def 3;

      ( rng ( canFS N1)) c= N1 by FINSEQ_1:def 4;

      then ( rng ( canFS N1)) c= ( Seg ( len G)) by XBOOLE_1: 1;

      then

       A15: ( canFS N1) is FinSequence of ( Seg ( len G)) by FINSEQ_1:def 4;

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

      then

       A16: s is Function of ( Seg ( len G)), Omega by A3, FUNCT_2: 1;

      then

      reconsider t1 = (s * ( canFS N1)) as FinSequence of Omega by A15, FINSEQ_2: 32;

      

       A17: ( rng t1) = (s .: ( rng ( canFS N1))) by RELAT_1: 127

      .= (s .: N1) by FUNCT_2:def 3

      .= Y by A3, FUNCT_1: 77;

      set N2 = (( Seg ( len G)) \ N1);

      reconsider N2 as finite Subset of ( Seg ( len G)) by XBOOLE_1: 36;

      ( rng ( canFS N2)) c= N2 by FINSEQ_1:def 4;

      then ( rng ( canFS N2)) c= ( Seg ( len G)) by XBOOLE_1: 1;

      then ( canFS N2) is FinSequence of ( Seg ( len G)) by FINSEQ_1:def 4;

      then

      reconsider t2 = (s * ( canFS N2)) as FinSequence of Omega by A16, FINSEQ_2: 32;

      reconsider t = (t1 ^ t2) as FinSequence of Omega;

      

       A18: ( rng ( canFS N1)) = N1 by FUNCT_2:def 3;

      

       A19: ( rng ( canFS N2)) = N2 by FUNCT_2:def 3;

      

       A20: N1 is finite Subset of ( dom s) & N2 is finite Subset of ( dom s) by A3, FINSEQ_1:def 3;

      then ( rng (s | N1)) misses ( rng (s | N2)) by Th1, A3, XBOOLE_1: 79;

      then ( rng t1) misses ( rng (s | N2)) by A18, Th2, XBOOLE_1: 63;

      then

       A21: ( rng t1) misses ( rng t2) by A19, Th2, XBOOLE_1: 63;

      then

       A22: t is one-to-one by A3, FINSEQ_3: 91;

      ( len ( canFS N1)) = ( card N1) by FINSEQ_1: 93;

      then

       A23: ( dom ( canFS N1)) = ( Seg ( card N1)) by FINSEQ_1:def 3;

      ( rng ( canFS N1)) is Subset of ( dom s) by A20, FUNCT_2:def 3;

      then ( dom t1) = ( Seg ( card N1)) by A23, RELAT_1: 27;

      then

       A24: ( len t1) = ( card N1) by FINSEQ_1:def 3;

      ( len ( canFS N2)) = ( card N2) by FINSEQ_1: 93;

      then

       A25: ( dom ( canFS N2)) = ( Seg ( card N2)) by FINSEQ_1:def 3;

      ( rng ( canFS N2)) is Subset of ( dom s) by A20, FUNCT_2:def 3;

      then ( dom t2) = ( Seg ( card N2)) by A25, RELAT_1: 27;

      then

       A26: ( len t2) = ( card N2) by FINSEQ_1:def 3;

      

       A27: (N1 \/ N2) = (( Seg ( len G)) \/ N1) by XBOOLE_1: 39

      .= ( Seg ( len G)) by XBOOLE_1: 12

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

      ( dom t) = ( Seg (( len t1) + ( len t2))) by FINSEQ_1:def 7

      .= ( Seg ( card (N1 \/ N2))) by A24, A26, CARD_2: 40, XBOOLE_1: 79;

      then

       A28: ( len t) = ( card (N1 \/ N2)) by FINSEQ_1:def 3;

      then

       A29: ( len t) = ( len s) by A27, CARD_1: 62;

      

       A30: ( Seg ( len s)) = ( Seg ( len t)) by A28, A27, CARD_1: 62;

      

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

      .= ( dom t) by A30, FINSEQ_1:def 3;

      

       A32: ( card ( dom t)) = ( card Omega) by A3, A29, CARD_1: 62;

      t is Function of ( dom t), Omega by FINSEQ_2: 26;

      then t is onto by A22, A32, FINSEQ_4: 63;

      then ( rng s) = ( rng t) by A3, FUNCT_2:def 3;

      then

      consider PN be Permutation of ( dom s) such that

       A33: t = (s * PN) & ( dom PN) = ( dom s) & ( rng PN) = ( dom s) by A3, A22, BHSP_5: 1;

      defpred FF1[ object, object] means ((t . $1) in Y implies $2 = ((f . (t . $1)) * (P . {(t . $1)}))) & (( not (t . $1) in Y) implies $2 = ((g . (t . $1)) * (P . {(t . $1)})));

       A34:

      now

        let k be Nat;

        assume k in ( Seg ( card Omega));

        now

          per cases ;

            suppose (t . k) in Y;

            hence ex x be Real st FF1[k, x];

          end;

            suppose not (t . k) in Y;

            hence ex x be Real st FF1[k, x];

          end;

        end;

        then

        consider x be Real such that

         A35: FF1[k, x];

        reconsider x as Element of REAL by XREAL_0:def 1;

        take x;

        thus FF1[k, x] by A35;

      end;

      consider F be FinSequence of REAL such that

       A36: ( dom F) = ( Seg ( card Omega)) and

       A37: for n be Nat st n in ( Seg ( card Omega)) holds FF1[n, (F . n)] from FINSEQ_1:sch 5( A34);

      

       A38: ( dom s) = ( Seg ( len G)) by A3, FINSEQ_1:def 3

      .= ( dom G) by FINSEQ_1:def 3;

      then

       A39: ( dom (G * PN)) = ( dom PN) by A33, RELAT_1: 27;

      

       A40: ( dom F) = ( dom s) by A3, A36, FINSEQ_1:def 3;

      now

        let x be object;

        assume

         A41: x in ( dom F);

        then

        reconsider nx = x as Element of NAT ;

        

         A42: nx in ( dom t) by A41, A3, A36, A31, FINSEQ_1:def 3;

        

         A43: (t . nx) = (s . (PN . nx)) by A33, A41, A40, A31, FUNCT_1: 12;

        (PN . nx) in ( dom G) by A38, A42, A33, FUNCT_1: 11;

        then

         A44: (G . (PN . nx)) = ((g . (s . (PN . nx))) * (P . {(s . (PN . nx))})) by A3;

        now

          per cases ;

            suppose

             A45: (t . nx) in Y;

            

            hence (F . nx) = ((f . (t . nx)) * (P . {(t . nx)})) by A37, A36, A41

            .= (((f | Y) . (s . (PN . nx))) * (P . {(s . (PN . nx))})) by A43, A45, FUNCT_1: 49

            .= ((g . (s . (PN . nx))) * (P . {(s . (PN . nx))})) by A45, A43, A9, FUNCT_1: 49

            .= ((G * PN) . nx) by A40, A41, A33, A44, FUNCT_1: 13;

          end;

            suppose not (t . nx) in Y;

            

            hence (F . nx) = ((g . (s . (PN . nx))) * (P . {(s . (PN . nx))})) by A43, A37, A36, A41

            .= ((G * PN) . nx) by A40, A41, A33, A44, FUNCT_1: 13;

          end;

        end;

        hence (F . x) = ((G * PN) . x);

      end;

      then F = (G * PN) by A33, A39, A40, FUNCT_1: 2;

      then

       A46: ( Sum G) = ( Sum F) by A38, FINSOP_1: 7;

      reconsider t1 as FinSequence of Y by A17, FINSEQ_1:def 4;

      reconsider F1 = (F | ( len t1)) as FinSequence of REAL ;

      reconsider F2 = (F /^ ( len t1)) as FinSequence of REAL ;

      

       A47: F = (F1 ^ F2) by RFINSEQ: 8;

      

       A48: ( len t1) = ( card Y) by A17, A3, FINSEQ_4: 62;

      

       A49: ( len F) = ( card Omega) by A36, FINSEQ_1:def 3;

      

       A50: ( len F) = ( len t) by A29, A3, A36, FINSEQ_1:def 3;

      

       A51: ( len t) = (( len t1) + ( len t2)) by FINSEQ_1: 22;

      then

       A52: ( len t1) <= ( len t) by NAT_1: 11;

      

      then

       A53: ( len F2) = (( len F) - ( len t1)) by A50, RFINSEQ:def 1

      .= ( len t2) by A51, A50;

      

      then

       A54: ( dom F2) = ( Seg ( len t2)) by FINSEQ_1:def 3

      .= ( dom (( len t2) |-> 0 )) by FUNCOP_1: 13;

      now

        let m be Nat;

        assume

         A55: m in ( dom F2);

        then

         A56: m in ( Seg ( len t2)) by A53, FINSEQ_1:def 3;

        then

         A57: m in ( dom t2) by FINSEQ_1:def 3;

        

         A58: 1 <= m & m <= ( len t2) by A56, FINSEQ_1: 1;

        m <= (m + ( len t1)) by NAT_1: 11;

        then 1 <= (m + ( len t1)) & (m + ( len t1)) <= ( len t) by A51, A58, XREAL_1: 6, XXREAL_0: 2;

        then

         A59: (m + ( len t1)) in ( Seg ( card Omega)) by A3, A29;

        

         A60: (t . (m + ( len t1))) = (t2 . m) by A57, FINSEQ_1:def 7;

        

         A61: (( rng t1) /\ ( rng t2)) = {} by A21, XBOOLE_0:def 7;

        

         A62: (t2 . m) in ( rng t2) by A57, FUNCT_1: 3;

        then not (t2 . m) in ( rng t1) by A61, XBOOLE_0:def 4;

        then

         A63: (t2 . m) in ( dom (g | YN)) by A10, A17, A62, XBOOLE_0:def 5;

        

        then

         A64: (g . (t2 . m)) = ((g | YN) . (t2 . m)) by FUNCT_1: 47

        .= 0 by A11, A63;

         not (t . (m + ( len t1))) in Y by A17, A61, A62, A60, XBOOLE_0:def 4;

        

        then

         A65: (F . (m + ( len t1))) = ((g . (t . (m + ( len t1)))) * (P . {(t . (m + ( len t1)))})) by A37, A59

        .= 0 by A64, A60;

        

        thus (F2 . m) = (F . (m + ( len t1))) by A50, A52, A55, RFINSEQ:def 1

        .= ((( len t2) |-> 0 ) . m) by A56, A65, FINSEQ_2: 57;

      end;

      then

       A66: F2 = (( len t2) |-> 0 ) by A54, FINSEQ_1: 13;

      ( Segm ( card Y)) c= ( Segm ( card Omega)) by CARD_1: 11;

      then

       A67: ( card Y) <= ( card Omega) by NAT_1: 39;

      

       A68: ( Sum F) = (( Sum F1) + ( Sum F2)) by A47, RVSUM_1: 75

      .= (( Sum F1) + 0 qua Real) by A66, RVSUM_1: 81

      .= ( Sum F1);

      

       A69: ( len F1) = ( card Y) by A49, A48, A67, FINSEQ_1: 59;

      for n be Nat st n in ( dom F1) holds (F1 . n) = ((f . (t1 . n)) * (P . {(t1 . n)}))

      proof

        let n be Nat;

        assume n in ( dom F1);

        then

         A70: n in ( Seg ( len t1)) by A69, A48, FINSEQ_1:def 3;

        then

         A71: n in ( dom t1) by FINSEQ_1:def 3;

        then

         A72: (t . n) = (t1 . n) by FINSEQ_1:def 7;

        then

         A73: (t . n) in Y by A17, A71, FUNCT_1: 3;

        

         A74: ( Seg ( len t1)) c= ( Seg ( card Omega)) by A48, A67, FINSEQ_1: 5;

        

        thus (F1 . n) = (F . n) by A70, FUNCT_1: 49

        .= ((f . (t1 . n)) * (P . {(t1 . n)})) by A72, A74, A70, A37, A73;

      end;

      hence thesis by A69, A48, A17, A68, A46, A3, A14;

    end;

    reconsider jj = 1 as R_eal by XXREAL_0:def 1;

    

     Lm7: for Omega1,Omega2 be non empty finite set, P1 be Probability of ( Trivial-SigmaField Omega1), P2 be Probability of ( Trivial-SigmaField Omega2), Q be Function of [:Omega1, Omega2:], REAL , P be Function of ( bool [:Omega1, Omega2:]), REAL , Y1 be non empty finite Subset of Omega1, Y2 be non empty finite Subset of Omega2 st (for x,y be set st x in Omega1 & y in Omega2 holds (Q . (x,y)) = ((P1 . {x}) * (P2 . {y}))) & (for z be finite Subset of [:Omega1, Omega2:] holds (P . z) = ( setopfunc (z, [:Omega1, Omega2:], REAL ,Q, addreal ))) holds (P . [:Y1, Y2:]) = ((P1 . Y1) * (P2 . Y2))

    proof

      let Omega1,Omega2 be non empty finite set, P1 be Probability of ( Trivial-SigmaField Omega1), P2 be Probability of ( Trivial-SigmaField Omega2), Q be Function of [:Omega1, Omega2:], REAL , P be Function of ( bool [:Omega1, Omega2:]), REAL , Y1 be non empty finite Subset of Omega1, Y2 be non empty finite Subset of Omega2;

      assume

       A1: (for x,y be set st x in Omega1 & y in Omega2 holds (Q . (x,y)) = ((P1 . {x}) * (P2 . {y}))) & (for z be finite Subset of [:Omega1, Omega2:] holds (P . z) = ( setopfunc (z, [:Omega1, Omega2:], REAL ,Q, addreal )));

      deffunc FF1( object) = (P1 . {$1});

      

       A2: for x be object st x in Y1 holds FF1(x) in REAL by XREAL_0:def 1;

      consider F1 be Function of Y1, REAL such that

       A3: for x be object st x in Y1 holds (F1 . x) = FF1(x) from FUNCT_2:sch 2( A2);

      deffunc FF2( object) = (P2 . {$1});

      

       A4: for x be object st x in Y2 holds FF2(x) in REAL by XREAL_0:def 1;

      consider F2 be Function of Y2, REAL such that

       A5: for x be object st x in Y2 holds (F2 . x) = FF2(x) from FUNCT_2:sch 2( A4);

      for x be object st x in { {} , 1} holds x in REAL by XREAL_0:def 1;

      then

       A6: { {} , 1} c= REAL ;

      

       A7: ( dom ( chi (Y1,Omega1))) = Omega1 & ( rng ( chi (Y1,Omega1))) c= { {} , 1} by FUNCT_3: 39, FUNCT_3:def 3;

      then ( chi (Y1,Omega1)) is Function of Omega1, { {} , 1} by FUNCT_2:def 1, RELSET_1: 4;

      then

      reconsider f1 = ( chi (Y1,Omega1)) as Function of Omega1, REAL by A6, FUNCT_2: 7;

      

       A8: ( dom (f1 | Y1)) = (( dom f1) /\ Y1) by RELAT_1: 61

      .= Y1 by A7, XBOOLE_1: 28;

      for x be object st x in ( dom (f1 | Y1)) holds ((f1 | Y1) . x) = 1

      proof

        let x be object;

        assume

         A9: x in ( dom (f1 | Y1));

        

        then ((f1 | Y1) . x) = (f1 . x) by FUNCT_1: 47

        .= 1 by A9, A8, FUNCT_3:def 3;

        hence thesis;

      end;

      

      then

       A10: ( Integral (( P2M P1),(f1 | Y1))) = (jj * (( P2M P1) . ( dom (f1 | Y1)))) by MESFUNC6: 97

      .= (1 * (P1 . Y1)) by A8, EXTREAL1: 1

      .= (P1 . Y1);

      consider G1 be FinSequence of REAL , s1 be FinSequence of Y1 such that

       A11: ( len G1) = ( card Y1) & s1 is one-to-one & ( rng s1) = Y1 & ( len s1) = ( card Y1) & (for n be Nat st n in ( dom G1) holds (G1 . n) = ((f1 . (s1 . n)) * (P1 . {(s1 . n)}))) & ( Integral (( P2M P1),(f1 | Y1))) = ( Sum G1) by Th15;

      Y1 c= Y1;

      then

      reconsider YY1 = Y1 as finite Subset of Y1;

      ( dom F1) = Y1 by FUNCT_2:def 1;

      then

       A12: ( dom (F1 * s1)) = ( dom s1) by A11, RELAT_1: 27;

      

       A13: ( dom G1) = ( Seg ( len s1)) by A11, FINSEQ_1:def 3

      .= ( dom s1) by FINSEQ_1:def 3;

      now

        let x be object;

        assume

         A14: x in ( dom G1);

        then

        reconsider nx = x as Element of NAT ;

        

         A15: (s1 . nx) in Y1 by A11, A13, A14, FUNCT_1: 3;

        

        thus (G1 . x) = ((f1 . (s1 . nx)) * (P1 . {(s1 . nx)})) by A11, A14

        .= (1 * (P1 . {(s1 . nx)})) by A15, FUNCT_3:def 3

        .= (F1 . (s1 . nx)) by A3, A11, A13, A14, FUNCT_1: 3

        .= ((F1 * s1) . x) by A13, A14, FUNCT_1: 13;

      end;

      then G1 = ( Func_Seq (F1,s1)) by A12, A13, FUNCT_1: 2;

      then

       A16: ( setopfunc (YY1,Y1, REAL ,F1, addreal )) = ( Sum G1) by A11, Th10;

      

       A17: ( dom ( chi (Y2,Omega2))) = Omega2 & ( rng ( chi (Y2,Omega2))) c= { {} , 1} by FUNCT_3: 39, FUNCT_3:def 3;

      then ( chi (Y2,Omega2)) is Function of Omega2, { {} , 1} by FUNCT_2:def 1, RELSET_1: 4;

      then

      reconsider f2 = ( chi (Y2,Omega2)) as Function of Omega2, REAL by A6, FUNCT_2: 7;

      

       A18: ( dom (f2 | Y2)) = (( dom f2) /\ Y2) by RELAT_1: 61

      .= Y2 by A17, XBOOLE_1: 28;

      for x be object st x in ( dom (f2 | Y2)) holds ((f2 | Y2) . x) = 1

      proof

        let x be object;

        assume

         A19: x in ( dom (f2 | Y2));

        

        then ((f2 | Y2) . x) = (f2 . x) by FUNCT_1: 47

        .= 1 by A19, A18, FUNCT_3:def 3;

        hence thesis;

      end;

      

      then

       A20: ( Integral (( P2M P2),(f2 | Y2))) = (jj * (( P2M P2) . Y2)) by A18, MESFUNC6: 97

      .= (1 * (P2 . Y2)) by EXTREAL1: 1

      .= (P2 . Y2);

      consider G2 be FinSequence of REAL , s2 be FinSequence of Y2 such that

       A21: ( len G2) = ( card Y2) & s2 is one-to-one & ( rng s2) = Y2 & ( len s2) = ( card Y2) & (for n be Nat st n in ( dom G2) holds (G2 . n) = ((f2 . (s2 . n)) * (P2 . {(s2 . n)}))) & ( Integral (( P2M P2),(f2 | Y2))) = ( Sum G2) by Th15;

      Y2 c= Y2;

      then

      reconsider YY2 = Y2 as finite Subset of Y2;

      ( dom F2) = Y2 by FUNCT_2:def 1;

      then

       A22: ( dom (F2 * s2)) = ( dom s2) by A21, RELAT_1: 27;

      

       A23: ( dom G2) = ( Seg ( len s2)) by A21, FINSEQ_1:def 3

      .= ( dom s2) by FINSEQ_1:def 3;

      now

        let x be object;

        assume

         A24: x in ( dom G2);

        then

        reconsider nx = x as Element of NAT ;

        

         A25: (s2 . nx) in Y2 by A21, A23, A24, FUNCT_1: 3;

        

        thus (G2 . x) = ((f2 . (s2 . nx)) * (P2 . {(s2 . nx)})) by A21, A24

        .= (1 * (P2 . {(s2 . nx)})) by A25, FUNCT_3:def 3

        .= (F2 . (s2 . nx)) by A5, A21, A23, A24, FUNCT_1: 3

        .= ((F2 * s2) . x) by A23, A24, FUNCT_1: 13;

      end;

      then G2 = ( Func_Seq (F2,s2)) by A22, A23, FUNCT_1: 2;

      then

       A26: ( setopfunc (YY2,Y2, REAL ,F2, addreal )) = ( Sum G2) by A21, Th10;

      reconsider Y3 = [:Y1, Y2:] as finite Subset of [:Y1, Y2:] by ZFMISC_1: 96;

      reconsider Y33 = [:Y1, Y2:] as finite Subset of [:Omega1, Omega2:] by ZFMISC_1: 96;

      

       A27: [:Y1, Y2:] c= [:Omega1, Omega2:] by ZFMISC_1: 96;

      then

      reconsider Q0 = (Q | [:Y1, Y2:]) as Function of [:Y1, Y2:], REAL by FUNCT_2: 32;

       A28:

      now

        let x,y be set;

        assume

         A29: x in Y1 & y in Y2;

        then [x, y] in [:Y1, Y2:] by ZFMISC_1:def 2;

        then [x, y] in ( dom Q0) by FUNCT_2:def 1;

        

        hence (Q0 . (x,y)) = (Q . (x,y)) by FUNCT_1: 47

        .= ((P1 . {x}) * (P2 . {y})) by A1, A29

        .= ((F1 . x) * (P2 . {y})) by A29, A3

        .= ((F1 . x) * (F2 . y)) by A29, A5;

      end;

      consider pp1 be FinSequence of [:Y1, Y2:] such that

       A30: pp1 is one-to-one & ( rng pp1) = Y3 & ( setopfunc (Y3, [:Y1, Y2:], REAL ,Q0, addreal )) = ( addreal "**" ( Func_Seq (Q0,pp1))) by BHSP_5:def 5;

      

       A31: ( rng pp1) c= [:Omega1, Omega2:] by A27;

      then

      reconsider pp2 = pp1 as FinSequence of [:Omega1, Omega2:] by FINSEQ_1:def 4;

      ( rng pp1) c= ( dom Q) by A31, FUNCT_2:def 1;

      then

       A32: ( dom (Q * pp1)) = ( dom pp1) by RELAT_1: 27;

      

       A33: ( dom Q0) = [:Y1, Y2:] by FUNCT_2:def 1;

      for x be object st x in ( dom (Q0 * pp1)) holds ((Q0 * pp1) . x) = ((Q * pp1) . x)

      proof

        let x be object;

        assume x in ( dom (Q0 * pp1));

        then

         A34: ((Q0 * pp1) . x) = (Q0 . (pp1 . x)) & x in ( dom pp1) by FUNCT_1: 11, FUNCT_1: 12;

        then (pp1 . x) in ( rng pp1) by FUNCT_1: 3;

        then (Q0 . (pp1 . x)) = (Q . (pp1 . x)) by FUNCT_1: 49;

        hence thesis by A34, FUNCT_1: 13;

      end;

      then

       A35: ( Func_Seq (Q0,pp1)) = ( Func_Seq (Q,pp2)) by A33, A32, A31, FUNCT_1: 2, RELAT_1: 27;

      

       A36: ( setopfunc (Y3, [:Y1, Y2:], REAL ,Q0, addreal )) = ( setopfunc (Y33, [:Omega1, Omega2:], REAL ,Q, addreal )) by A30, A35, BHSP_5:def 5;

      

      thus (P . [:Y1, Y2:]) = ( setopfunc (Y33, [:Omega1, Omega2:], REAL ,Q, addreal )) by A1

      .= ((P1 . Y1) * (P2 . Y2)) by A20, A21, A10, A11, A26, A16, Th12, A28, A36;

    end;

    

     Lm8: for Omega1,Omega2 be non empty finite set, P1 be Probability of ( Trivial-SigmaField Omega1), P2 be Probability of ( Trivial-SigmaField Omega2), Q be Function of [:Omega1, Omega2:], REAL , P be Function of ( bool [:Omega1, Omega2:]), REAL st (for x,y be set st x in Omega1 & y in Omega2 holds (Q . (x,y)) = ((P1 . {x}) * (P2 . {y}))) & (for z be finite Subset of [:Omega1, Omega2:] holds (P . z) = ( setopfunc (z, [:Omega1, Omega2:], REAL ,Q, addreal ))) holds (P . [:Omega1, Omega2:]) = 1

    proof

      let Omega1,Omega2 be non empty finite set, P1 be Probability of ( Trivial-SigmaField Omega1), P2 be Probability of ( Trivial-SigmaField Omega2), Q be Function of [:Omega1, Omega2:], REAL , P be Function of ( bool [:Omega1, Omega2:]), REAL ;

      assume

       A1: (for x,y be set st x in Omega1 & y in Omega2 holds (Q . (x,y)) = ((P1 . {x}) * (P2 . {y}))) & (for z be finite Subset of [:Omega1, Omega2:] holds (P . z) = ( setopfunc (z, [:Omega1, Omega2:], REAL ,Q, addreal )));

      deffunc FF1( object) = (P1 . {$1});

      

       A2: for x be object st x in Omega1 holds FF1(x) in REAL by XREAL_0:def 1;

      consider F1 be Function of Omega1, REAL such that

       A3: for x be object st x in Omega1 holds (F1 . x) = FF1(x) from FUNCT_2:sch 2( A2);

      deffunc FF2( object) = (P2 . {$1});

      

       A4: for x be object st x in Omega2 holds FF2(x) in REAL by XREAL_0:def 1;

      consider F2 be Function of Omega2, REAL such that

       A5: for x be object st x in Omega2 holds (F2 . x) = FF2(x) from FUNCT_2:sch 2( A4);

      

       A6: ( dom (Omega1 --> 1)) = Omega1 by FUNCOP_1: 13;

      ( rng (Omega1 --> 1)) c= REAL ;

      then

      reconsider f1 = (Omega1 --> 1) as Function of Omega1, REAL by A6, FUNCT_2: 2;

      for x be object st x in ( dom (Omega1 --> 1)) holds ((Omega1 --> 1) . x) = 1 by FUNCOP_1: 7;

      

      then

       A7: ( Integral (( P2M P1),f1)) = (jj * (( P2M P1) . Omega1)) by A6, MESFUNC6: 97

      .= (1 * (P1 . Omega1)) by EXTREAL1: 1

      .= 1 by PROB_1:def 8;

      consider G1 be FinSequence of REAL , s1 be FinSequence of Omega1 such that

       A8: ( len G1) = ( card Omega1) & s1 is one-to-one & ( rng s1) = Omega1 & ( len s1) = ( card Omega1) & (for n be Nat st n in ( dom G1) holds (G1 . n) = ((f1 . (s1 . n)) * (P1 . {(s1 . n)}))) & ( Integral (( P2M P1),f1)) = ( Sum G1) by RANDOM_1: 13;

      Omega1 c= Omega1;

      then

      reconsider Y1 = Omega1 as finite Subset of Omega1;

      ( dom F1) = Y1 by FUNCT_2:def 1;

      then

       A9: ( dom (F1 * s1)) = ( dom s1) by A8, RELAT_1: 27;

      

       A10: ( dom G1) = ( Seg ( len s1)) by A8, FINSEQ_1:def 3

      .= ( dom s1) by FINSEQ_1:def 3;

      now

        let x be object;

        assume

         A11: x in ( dom G1);

        then

        reconsider nx = x as Element of NAT ;

        

        thus (G1 . x) = ((f1 . (s1 . nx)) * (P1 . {(s1 . nx)})) by A8, A11

        .= (1 * (P1 . {(s1 . nx)})) by A8, A10, A11, FUNCOP_1: 7, FUNCT_1: 3

        .= (F1 . (s1 . nx)) by A3, A8, A10, A11, FUNCT_1: 3

        .= ((F1 * s1) . x) by A10, A11, FUNCT_1: 13;

      end;

      then G1 = ( Func_Seq (F1,s1)) by A9, A10, FUNCT_1: 2;

      then

       A12: ( setopfunc (Y1,Omega1, REAL ,F1, addreal )) = 1 by A7, A8, Th10;

      

       A13: ( dom (Omega2 --> 1)) = Omega2 by FUNCOP_1: 13;

      ( rng (Omega2 --> 1)) c= REAL ;

      then

      reconsider f2 = (Omega2 --> 1) as Function of Omega2, REAL by A13, FUNCT_2: 2;

      for x be object st x in ( dom (Omega2 --> 1)) holds ((Omega2 --> 1) . x) = 1 by FUNCOP_1: 7;

      

      then

       A14: ( Integral (( P2M P2),f2)) = (jj * (( P2M P2) . Omega2)) by A13, MESFUNC6: 97

      .= (1 * (P2 . Omega2)) by EXTREAL1: 1

      .= 1 by PROB_1:def 8;

      consider G2 be FinSequence of REAL , s2 be FinSequence of Omega2 such that

       A15: ( len G2) = ( card Omega2) & s2 is one-to-one & ( rng s2) = Omega2 & ( len s2) = ( card Omega2) & (for n be Nat st n in ( dom G2) holds (G2 . n) = ((f2 . (s2 . n)) * (P2 . {(s2 . n)}))) & ( Integral (( P2M P2),f2)) = ( Sum G2) by RANDOM_1: 13;

      Omega2 c= Omega2;

      then

      reconsider Y2 = Omega2 as finite Subset of Omega2;

      ( dom F2) = Y2 by FUNCT_2:def 1;

      then

       A16: ( dom (F2 * s2)) = ( dom s2) by A15, RELAT_1: 27;

      

       A17: ( dom G2) = ( Seg ( len s2)) by A15, FINSEQ_1:def 3

      .= ( dom s2) by FINSEQ_1:def 3;

      now

        let x be object;

        assume

         A18: x in ( dom G2);

        then

        reconsider nx = x as Element of NAT ;

        

        thus (G2 . x) = ((f2 . (s2 . nx)) * (P2 . {(s2 . nx)})) by A15, A18

        .= (1 * (P2 . {(s2 . nx)})) by A15, A17, A18, FUNCOP_1: 7, FUNCT_1: 3

        .= (F2 . (s2 . nx)) by A5, A15, A17, A18, FUNCT_1: 3

        .= ((F2 * s2) . x) by A17, A18, FUNCT_1: 13;

      end;

      then

       A19: G2 = ( Func_Seq (F2,s2)) by A16, A17, FUNCT_1: 2;

      reconsider Y3 = [:Y1, Y2:] as finite Subset of [:Omega1, Omega2:] by ZFMISC_1: 96;

       A20:

      now

        let x,y be set;

        assume

         A21: x in Y1 & y in Y2;

        

        hence (Q . (x,y)) = ((P1 . {x}) * (P2 . {y})) by A1

        .= ((F1 . x) * (P2 . {y})) by A21, A3

        .= ((F1 . x) * (F2 . y)) by A21, A5;

      end;

      

      thus (P . [:Omega1, Omega2:]) = ( setopfunc (Y3, [:Omega1, Omega2:], REAL ,Q, addreal )) by A1

      .= (( setopfunc (Y1,Omega1, REAL ,F1, addreal )) * ( setopfunc (Y2,Omega2, REAL ,F2, addreal ))) by Th12, A20

      .= 1 by A19, A14, A15, Th10, A12;

    end;

    

     Lm9: for Omega1,Omega2 be non empty finite set, P1 be Probability of ( Trivial-SigmaField Omega1), P2 be Probability of ( Trivial-SigmaField Omega2), Q be Function of [:Omega1, Omega2:], REAL , P be Function of ( bool [:Omega1, Omega2:]), REAL st (for x,y be set st x in Omega1 & y in Omega2 holds (Q . (x,y)) = ((P1 . {x}) * (P2 . {y}))) & (for z be finite Subset of [:Omega1, Omega2:] holds (P . z) = ( setopfunc (z, [:Omega1, Omega2:], REAL ,Q, addreal ))) holds for x be set st x c= [:Omega1, Omega2:] holds 0 <= (P . x) & (P . x) <= 1

    proof

      let Omega1,Omega2 be non empty finite set, P1 be Probability of ( Trivial-SigmaField Omega1), P2 be Probability of ( Trivial-SigmaField Omega2), Q be Function of [:Omega1, Omega2:], REAL , P be Function of ( bool [:Omega1, Omega2:]), REAL ;

      assume

       A1: (for x,y be set st x in Omega1 & y in Omega2 holds (Q . (x,y)) = ((P1 . {x}) * (P2 . {y}))) & (for z be finite Subset of [:Omega1, Omega2:] holds (P . z) = ( setopfunc (z, [:Omega1, Omega2:], REAL ,Q, addreal )));

      reconsider Y12 = [:Omega1, Omega2:] as finite Subset of [:Omega1, Omega2:] by SUBSET: 3;

       A2:

      now

        let z be set;

        assume z in [:Omega1, Omega2:];

        then

        consider x,y be object such that

         A3: x in Omega1 & y in Omega2 & z = [x, y] by ZFMISC_1:def 2;

        for xx be object st xx in {x} holds xx in Omega1 by A3, TARSKI:def 1;

        then

         A4: {x} is Event of ( Trivial-SigmaField Omega1) & for xx be object st xx in {y} holds xx in Omega2 by A3, TARSKI:def 1, TARSKI:def 3;

        then

         A5: {y} is Event of ( Trivial-SigmaField Omega2) by TARSKI:def 3;

        

         A6: (Q . z) = (Q . (x,y)) by A3

        .= ((P1 . {x}) * (P2 . {y})) by A3, A1;

         0 <= (P1 . {x}) & 0 <= (P2 . {y}) by A4, A5, PROB_1:def 8;

        hence 0 <= (Q . z) by A6;

      end;

      let x be set;

      assume x c= [:Omega1, Omega2:];

      then

      reconsider Y = x as finite Subset of [:Omega1, Omega2:];

      for z be set st z in Y holds 0 <= (Q . z) by A2;

      then 0 <= ( setopfunc (Y, [:Omega1, Omega2:], REAL ,Q, addreal )) by Th13;

      hence 0 <= (P . x) by A1;

      

       A7: ( setopfunc (Y, [:Omega1, Omega2:], REAL ,Q, addreal )) <= ( setopfunc (Y12, [:Omega1, Omega2:], REAL ,Q, addreal )) by A2, Th14;

      ( setopfunc (Y12, [:Omega1, Omega2:], REAL ,Q, addreal )) = (P . [:Omega1, Omega2:]) by A1;

      then ( setopfunc (Y, [:Omega1, Omega2:], REAL ,Q, addreal )) <= 1 by A7, A1, Lm8;

      hence (P . x) <= 1 by A1;

    end;

    definition

      let Omega1,Omega2 be non empty finite set, P1 be Probability of ( Trivial-SigmaField Omega1), P2 be Probability of ( Trivial-SigmaField Omega2);

      :: RANDOM_2:def2

      func Product-Probability (Omega1,Omega2,P1,P2) -> Probability of ( Trivial-SigmaField [:Omega1, Omega2:]) means

      : Def2: ex Q be Function of [:Omega1, Omega2:], REAL st (for x,y be set st x in Omega1 & y in Omega2 holds (Q . (x,y)) = ((P1 . {x}) * (P2 . {y}))) & (for z be finite Subset of [:Omega1, Omega2:] holds (it . z) = ( setopfunc (z, [:Omega1, Omega2:], REAL ,Q, addreal )));

      existence

      proof

        consider Q be Function of [:Omega1, Omega2:], REAL such that

         A1: for x,y be set st x in Omega1 & y in Omega2 holds (Q . (x,y)) = ((P1 . {x}) * (P2 . {y})) by Lm1;

        consider P be Function of ( bool [:Omega1, Omega2:]), REAL such that

         A2: for z be finite Subset of [:Omega1, Omega2:] holds (P . z) = ( setopfunc (z, [:Omega1, Omega2:], REAL ,Q, addreal )) by Lm3;

        

         A3: for x be set st x c= [:Omega1, Omega2:] holds 0 <= (P . x) & (P . x) <= 1 by Lm9, A1, A2;

        (P . [:Omega1, Omega2:]) = 1 by A1, A2, Lm8;

        then P is Probability of ( Trivial-SigmaField [:Omega1, Omega2:]) by A2, A3, Th8;

        hence thesis by A1, A2;

      end;

      uniqueness

      proof

        let PP1,PP2 be Probability of ( Trivial-SigmaField [:Omega1, Omega2:]);

        assume

         A4: ex Q1 be Function of [:Omega1, Omega2:], REAL st (for x,y be set st x in Omega1 & y in Omega2 holds (Q1 . (x,y)) = ((P1 . {x}) * (P2 . {y}))) & (for z be finite Subset of [:Omega1, Omega2:] holds (PP1 . z) = ( setopfunc (z, [:Omega1, Omega2:], REAL ,Q1, addreal )));

        assume

         A5: ex Q2 be Function of [:Omega1, Omega2:], REAL st (for x,y be set st x in Omega1 & y in Omega2 holds (Q2 . (x,y)) = ((P1 . {x}) * (P2 . {y}))) & (for z be finite Subset of [:Omega1, Omega2:] holds (PP2 . z) = ( setopfunc (z, [:Omega1, Omega2:], REAL ,Q2, addreal )));

        consider Q1 be Function of [:Omega1, Omega2:], REAL such that

         A6: (for x,y be set st x in Omega1 & y in Omega2 holds (Q1 . (x,y)) = ((P1 . {x}) * (P2 . {y}))) & (for z be finite Subset of [:Omega1, Omega2:] holds (PP1 . z) = ( setopfunc (z, [:Omega1, Omega2:], REAL ,Q1, addreal ))) by A4;

        consider Q2 be Function of [:Omega1, Omega2:], REAL such that

         A7: (for x,y be set st x in Omega1 & y in Omega2 holds (Q2 . (x,y)) = ((P1 . {x}) * (P2 . {y}))) & (for z be finite Subset of [:Omega1, Omega2:] holds (PP2 . z) = ( setopfunc (z, [:Omega1, Omega2:], REAL ,Q2, addreal ))) by A5;

        Q1 = Q2 by A6, A7, Lm2;

        hence PP1 = PP2 by Lm4, A6, A7;

      end;

    end

    theorem :: RANDOM_2:16

    

     Th16: for Omega1,Omega2 be non empty finite set, P1 be Probability of ( Trivial-SigmaField Omega1), P2 be Probability of ( Trivial-SigmaField Omega2), Y1 be non empty finite Subset of Omega1, Y2 be non empty finite Subset of Omega2 holds (( Product-Probability (Omega1,Omega2,P1,P2)) . [:Y1, Y2:]) = ((P1 . Y1) * (P2 . Y2))

    proof

      let Omega1,Omega2 be non empty finite set, P1 be Probability of ( Trivial-SigmaField Omega1), P2 be Probability of ( Trivial-SigmaField Omega2), Y1 be non empty finite Subset of Omega1, Y2 be non empty finite Subset of Omega2;

      set P = ( Product-Probability (Omega1,Omega2,P1,P2));

      consider Q be Function of [:Omega1, Omega2:], REAL such that

       A1: (for x,y be set st x in Omega1 & y in Omega2 holds (Q . (x,y)) = ((P1 . {x}) * (P2 . {y}))) & (for z be finite Subset of [:Omega1, Omega2:] holds (P . z) = ( setopfunc (z, [:Omega1, Omega2:], REAL ,Q, addreal ))) by Def2;

      thus (P . [:Y1, Y2:]) = ((P1 . Y1) * (P2 . Y2)) by Lm7, A1;

    end;

    theorem :: RANDOM_2:17

    for Omega1,Omega2 be non empty finite set, P1 be Probability of ( Trivial-SigmaField Omega1), P2 be Probability of ( Trivial-SigmaField Omega2), y1,y2 be set st y1 in Omega1 & y2 in Omega2 holds (( Product-Probability (Omega1,Omega2,P1,P2)) . { [y1, y2]}) = ((P1 . {y1}) * (P2 . {y2}))

    proof

      let Omega1,Omega2 be non empty finite set, P1 be Probability of ( Trivial-SigmaField Omega1), P2 be Probability of ( Trivial-SigmaField Omega2), y1,y2 be set;

      assume

       A1: y1 in Omega1 & y2 in Omega2;

      then

       A2: {y1} is finite Subset of Omega1 by ZFMISC_1: 31;

      for yy be object st yy in {y2} holds yy in Omega2 by A1, TARSKI:def 1;

      then

       A3: {y2} is finite Subset of Omega2 by TARSKI:def 3;

       [: {y1}, {y2}:] = { [y1, y2]} by ZFMISC_1: 29;

      hence (( Product-Probability (Omega1,Omega2,P1,P2)) . { [y1, y2]}) = ((P1 . {y1}) * (P2 . {y2})) by Th16, A2, A3;

    end;

    begin

    definition

      let Omega be non empty set;

      let Sigma be SigmaField of Omega;

      :: RANDOM_2:def3

      func Real-Valued-Random-Variables-Set Sigma -> non empty Subset of ( RAlgebra Omega) equals the set of all f where f be Real-Valued-Random-Variable of Sigma;

      correctness

      proof

        

         A1: the set of all f where f be Real-Valued-Random-Variable of Sigma is non empty

        proof

          set g = the Real-Valued-Random-Variable of Sigma;

          g in the set of all f where f be Real-Valued-Random-Variable of Sigma;

          hence thesis;

        end;

         the set of all f where f be Real-Valued-Random-Variable of Sigma c= ( Funcs (Omega, REAL ))

        proof

          let x be object;

          assume x in the set of all f where f be Real-Valued-Random-Variable of Sigma;

          then

          consider f be Real-Valued-Random-Variable of Sigma such that

           A2: x = f;

          thus thesis by A2, FUNCT_2: 8;

        end;

        hence thesis by A1;

      end;

    end

    

     Lm10: ( Real-Valued-Random-Variables-Set Sigma) is additively-linearly-closed multiplicatively-closed

    proof

      set W = ( Real-Valued-Random-Variables-Set Sigma);

      set V = ( RAlgebra Omega);

      

       A1: for v,u be Element of V st v in W & u in W holds (v * u) in W

      proof

        let v,u be Element of V such that

         A2: v in W and

         A3: u in W;

        consider u1 be Real-Valued-Random-Variable of Sigma such that

         A4: u1 = u by A3;

        reconsider h = (v * u) as Element of ( Funcs (Omega, REAL ));

        consider v1 be Real-Valued-Random-Variable of Sigma such that

         A5: v1 = v by A2;

        (( dom v1) /\ ( dom u1)) = (Omega /\ ( dom u1)) by FUNCT_2:def 1;

        then

         A6: (ex f be Function st h = f & ( dom f) = Omega & ( rng f) c= REAL ) & (( dom v1) /\ ( dom u1)) = (Omega /\ Omega) by FUNCT_2:def 1, FUNCT_2:def 2;

        for x be object st x in ( dom h) holds (h . x) = ((v1 . x) * (u1 . x) qua Complex) by A5, A4, FUNCSDOM: 2;

        then (v * u) = (v1 (#) u1) by A6, VALUED_1:def 4;

        hence thesis;

      end;

      for v,u be Element of V st v in W & u in W holds (v + u) in W

      proof

        let v,u be Element of V such that

         A7: v in W and

         A8: u in W;

        consider u1 be Real-Valued-Random-Variable of Sigma such that

         A9: u1 = u by A8;

        reconsider h = (v + u) as Element of ( Funcs (Omega, REAL ));

        consider v1 be Real-Valued-Random-Variable of Sigma such that

         A10: v1 = v by A7;

        (( dom v1) /\ ( dom u1)) = (Omega /\ ( dom u1)) by FUNCT_2:def 1;

        then

         A11: (ex f be Function st h = f & ( dom f) = Omega & ( rng f) c= REAL ) & (( dom v1) /\ ( dom u1)) = (Omega /\ Omega) by FUNCT_2:def 1, FUNCT_2:def 2;

        for x be object st x in ( dom h) holds (h . x) = ((v1 . x) + (u1 . x) qua Real) by A10, A9, FUNCSDOM: 1;

        then (v + u) = (v1 + u1) by A11, VALUED_1:def 1;

        hence thesis;

      end;

      then

       A12: W is add-closed by IDEAL_1:def 1;

      

       A13: ( RAlgebra Omega) is RealLinearSpace by C0SP1: 7;

      for v be Element of V st v in W holds ( - v) in W

      proof

        let v be Element of V;

        assume v in W;

        then

        consider v1 be Real-Valued-Random-Variable of Sigma such that

         A14: v1 = v;

        

         A15: ( - v1) is Real-Valued-Random-Variable of Sigma by RANDOM_1: 20;

        reconsider h = ( - v) as Element of ( Funcs (Omega, REAL ));

        

         A16: h = (( - 1) * v) by A13, RLVECT_1: 16;

         A17:

        now

          let x be object;

          assume x in ( dom h);

          then

          reconsider y = x as Element of Omega;

          

          thus (h . x) = (( - 1) * (v1 . y)) by A16, A14, FUNCSDOM: 4

          .= ( - (v1 . x) qua Real);

        end;

        (ex f be Function st h = f & ( dom f) = Omega & ( rng f) c= REAL ) & ( dom v1) = Omega by FUNCT_2:def 1, FUNCT_2:def 2;

        then ( - v) = ( - v1) by A17, VALUED_1: 9;

        hence thesis by A15;

      end;

      then

       A18: W is having-inverse by C0SP1:def 1;

      for a be Real, u be Element of V st u in W holds (a * u) in W

      proof

        let a be Real, u be Element of V;

        assume u in W;

        then

        consider u1 be Real-Valued-Random-Variable of Sigma such that

         A19: u1 = u;

        reconsider h = (a * u) as Element of ( Funcs (Omega, REAL ));

        

         A20: (ex f be Function st h = f & ( dom f) = Omega & ( rng f) c= REAL ) & ( dom u1) = Omega by FUNCT_2:def 1, FUNCT_2:def 2;

        for x be object st x in ( dom h) holds (h . x) = (a * (u1 . x)) by A19, FUNCSDOM: 4;

        then (a * u) = (a (#) u1) by A20, VALUED_1:def 5;

        hence thesis;

      end;

      hence ( Real-Valued-Random-Variables-Set Sigma) is additively-linearly-closed by A12, A18, C0SP1:def 10;

      reconsider g = ( RealFuncUnit Omega) as Function of Omega, REAL ;

      g is Real-Valued-Random-Variable of Sigma by Th4;

      then ( 1. V) in W;

      hence thesis by A1, C0SP1:def 4;

    end;

    registration

      let Omega, Sigma;

      cluster ( Real-Valued-Random-Variables-Set Sigma) -> additively-linearly-closed multiplicatively-closed;

      coherence by Lm10;

    end

    definition

      let Omega, Sigma;

      :: RANDOM_2:def4

      func R_Algebra_of_Real-Valued-Random-Variables Sigma -> Algebra equals AlgebraStr (# ( Real-Valued-Random-Variables-Set Sigma), ( mult_ (( Real-Valued-Random-Variables-Set Sigma),( RAlgebra Omega))), ( Add_ (( Real-Valued-Random-Variables-Set Sigma),( RAlgebra Omega))), ( Mult_ (( Real-Valued-Random-Variables-Set Sigma),( RAlgebra Omega))), ( One_ (( Real-Valued-Random-Variables-Set Sigma),( RAlgebra Omega))), ( Zero_ (( Real-Valued-Random-Variables-Set Sigma),( RAlgebra Omega))) #);

      coherence by C0SP1: 6;

    end

    registration

      let Omega, Sigma;

      cluster ( R_Algebra_of_Real-Valued-Random-Variables Sigma) -> scalar-unital;

      coherence

      proof

        let v be VECTOR of ( R_Algebra_of_Real-Valued-Random-Variables Sigma);

        reconsider v1 = v as VECTOR of ( RAlgebra Omega) by TARSKI:def 3;

        ( R_Algebra_of_Real-Valued-Random-Variables Sigma) is Subalgebra of ( RAlgebra Omega) by C0SP1: 6;

        then (1 * v) = (1 * v1) by C0SP1: 8;

        hence (1 * v) = v by FUNCSDOM: 12;

      end;

    end