FINANCE3

:: Modelling Real World Using Stochastic Processes and Filtration
::  by Peter Jaeger
::
:: Received December 30, 2015
:: Copyright (c) 2015-2026 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies FINANCE1, SERIES_1, SEQ_1, RANDOM_3, FINANCE2, NUMBERS, XBOOLE_0,
      PROB_1, SUBSET_1, REAL_1, TARSKI, RELAT_1, FUNCT_1, ARYTM_3, XXREAL_0,
      VALUED_1, ARYTM_1, NAT_1, CARD_1, ZFMISC_1, RPR_1, SETFAM_1, FINANCE3,
      EQREL_1, FUNCOP_1, KOLMOG01, FUNCT_7, MEMBERED, RANDOM_1;
 notations TARSKI, SUBSET_1, XBOOLE_0,
      ORDINAL1, SERIES_1, SEQ_1, SETFAM_1, ENUMSET1,
      RELAT_1, FINANCE1, RANDOM_3, NUMBERS, XREAL_0, XXREAL_0, XCMPLX_0,
      MEMBERED, FUNCT_1, VALUED_1, NAT_1, FUNCT_2, PROB_1, SEQ_4, FINANCE2,
      RELSET_1, FUNCOP_1, KOLMOG01, RANDOM_1;
 constructors SERIES_1, REAL_1, RELSET_1, SEQ_4, FINANCE2, ENUMSET1, RANDOM_2,
      KOLMOG01, RANDOM_1, RANDOM_3;
 registrations PROB_1, FINANCE1, SUBSET_1, NAT_1, XREAL_0, MEMBERED, ORDINAL1,
      FUNCT_2, NUMBERS, VALUED_0, VALUED_1, RELSET_1, INT_1, XBOOLE_0;
 requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
 definitions TARSKI, FINANCE1;
 equalities FINANCE1, SUBSET_1, XCMPLX_0, FINANCE2;
 expansions FUNCT_2, TARSKI, XBOOLE_0, PROB_1, FINANCE1;
 theorems SERIES_1, FINANCE1, RANDOM_3, TARSKI, XBOOLE_0, PROB_1, NAT_1,
      FUNCT_2, VALUED_1, XREAL_0, FUNCT_1, NUMBERS, SUBSET_1, ZFMISC_1,
      ENUMSET1, FINANCE2, FUNCOP_1, RELAT_1, KOLMOG01, XBOOLE_1, ORDINAL1;
 schemes NAT_1, FUNCT_2;

begin

Lemacik:
for a,b,c being set st (a = 1 or a = 2 or a = 3 or a = 4) &
  (b = 1 or b = 2 or b = 3 or b = 4) &
  (c = 1 or c = 2 or c = 3 or c = 4) holds
  {a,b,c} c= {1,2,3,4}
proof
  let a,b,c be set;
  assume
A1:  (a = 1 or a = 2 or a = 3 or a = 4) &
  (b = 1 or b = 2 or b = 3 or b = 4) &
  (c = 1 or c = 2 or c = 3 or c = 4);
  for x being object st x in {a,b,c} holds x in {1,2,3,4}
  proof
   let x be object;
   assume x in {a,b,c}; then
   x = a or x = b or x = c by ENUMSET1:def 1;
   hence thesis by ENUMSET1:def 2,A1;
  end;
  hence thesis;
end;

Lemacik2:
for a,b being set st (a = 1 or a = 2 or a = 3 or a = 4) &
  (b = 1 or b = 2 or b = 3 or b = 4) holds
  {a,b} c= {1,2,3,4}
proof
  let a,b be set;
  assume
A1:  (a = 1 or a = 2 or a = 3 or a = 4) &
  (b = 1 or b = 2 or b = 3 or b = 4);
  for x being object st x in {a,b} holds x in {1,2,3,4}
  proof
   let x be object;
   assume x in {a,b}; then
   x = a or x = b by TARSKI:def 2;
   hence thesis by ENUMSET1:def 2,A1;
  end;
  hence thesis;
end;

Lemacik3:
for a being set st a = 1 or a = 2 or a = 3 or a = 4 holds
  {a} c= {1,2,3,4}
proof
  let a be set;
  assume
A1:  a = 1 or a = 2 or a = 3 or a = 4;
  for x being object st x in {a} holds x in {1,2,3,4}
  proof
   let x be object;
   assume x in {a}; then
   x = a by TARSKI:def 1;
   hence thesis by ENUMSET1:def 2,A1;
  end;
  hence thesis;
end;

The1: for A1 being SetSequence of {1,2,3,4} st
      (ex n being Nat st A1.n = {}) holds Intersection A1 = {}
      proof
        let A1 be SetSequence of {1,2,3,4};
        given n being Nat such that
AB:     A1.n = {};
        assume Intersection A1 <> {}; then
        consider x being object such that
AA:     x in Intersection A1 by XBOOLE_0:def 1;
        thus thesis by AB,PROB_1:13,AA;
      end;

EnLm1: {1} c= {1,2,3,4} by Lemacik3;
EnLm2: {2} c= {1,2,3,4} by Lemacik3;
EnLm3: {3} c= {1,2,3,4} by Lemacik3;
EnLm4: {4} c= {1,2,3,4} by Lemacik3;

theorem
  for a, b being object st a <> b holds
    {a} c< {a,b} by ZFMISC_1:7,20;

Lm1: {3,4} c= {1,2,3,4} by Lemacik2;
Lm2: {1,2} c= {1,2,3,4} by Lemacik2;

Lm3:
  {1,2} /\ {3,4} = {}
  proof
    {1,2} /\ {3,4} c= {}
    proof
      let x be object;
      x in {1,2} /\ {3,4} iff
        (x in {1,2} & x in {3,4}) by XBOOLE_0:def 4; then
      x in {1,2} /\ {3,4} iff
        ( (x = 1 or x = 2) & (x = 3 or x = 4)) by TARSKI:def 2;
      hence thesis;
    end;
    hence thesis;
  end;

Lem1: {1,2,3,4} \ {1,2} = {3,4}
proof
  for x being object holds x in {1,2,3,4} \ {1,2} iff x in {3,4}
  proof
    let x be object;
    thus x in {1,2,3,4} \ {1,2} implies x in {3,4}
    proof
      assume x in {1,2,3,4} \ {1,2}; then
        x in {1,2,3,4} & not x in {1,2} by XBOOLE_0:def 5; then
      (x = 1 or x = 2 or x = 3 or x = 4) & (x <> 1 & x <> 2) by TARSKI:def 2,
        ENUMSET1:def 2;
      hence thesis by TARSKI:def 2;
    end;
    assume x in {3,4}; then
    x = 3 or x = 4 by TARSKI:def 2; then
    x in {1,2,3,4} & not x in {1,2} by TARSKI:def 2,ENUMSET1:def 2;
    hence thesis by XBOOLE_0:def 5;
  end;
  hence thesis by TARSKI:2;
end;

Lem2: {1,2,3,4} \ {3,4} = {1,2}
proof
  for x being object holds x in {1,2,3,4} \ {3,4} iff x in {1,2}
  proof
    let x be object;
    thus x in {1,2,3,4} \ {3,4} implies x in {1,2}
    proof
      assume x in {1,2,3,4} \ {3,4}; then
        x in {1,2,3,4} & not x in {3,4} by XBOOLE_0:def 5; then
      (x = 1 or x = 2 or x = 3 or x = 4) & (x <> 3 & x <> 4) by TARSKI:def 2,
        ENUMSET1:def 2;
      hence thesis by TARSKI:def 2;
    end;
    assume x in {1,2}; then
    x = 1 or x = 2 by TARSKI:def 2; then
    x in {1,2,3,4} & not x in {3,4} by TARSKI:def 2,ENUMSET1:def 2;
    hence thesis by XBOOLE_0:def 5;
  end;
  hence thesis by TARSKI:2;
end;

B13: {1,3} in bool {1,2,3,4}
   proof
    {1,3} c= {1,2,3,4} by Lemacik2;
    hence thesis;
   end;

B14: {1,4} in bool {1,2,3,4}
   proof
     {1,4} c= {1,2,3,4} by Lemacik2;
     hence thesis;
   end;

B124: {1,2,4} in bool {1,2,3,4}
    proof
      {1,2,4} c= {1,2,3,4} by Lemacik;
      hence thesis;
    end;

B134: {1,3,4} in bool {1,2,3,4}
      proof
        {1,3,4} c= {1,2,3,4} by Lemacik;
        hence thesis;
      end;

B234:{2,3,4} in bool {1,2,3,4}
     proof
       {2,3,4} c= {1,2,3,4} by Lemacik;
       hence thesis;
     end;

B123: {1,2,3} in bool {1,2,3,4}
    proof
     {1,2,3} c= {1,2,3,4} by Lemacik;
      hence thesis;
    end;

B23: {2,3} in bool {1,2,3,4}
   proof
    {2,3} c= {1,2,3,4} by Lemacik2;
   hence thesis;
   end;

B24: {2,4} in bool {1,2,3,4}
   proof
     {2,4} c= {1,2,3,4} by Lemacik2;
     hence thesis;
   end;

B25: {1,2} in bool {1,2,3,4}
   proof
     {1,2} c= {1,2,3,4} by Lemacik2;
     hence thesis;
   end;

B26: {3,4} in bool {1,2,3,4}
   proof
     {3,4} c= {1,2,3,4} by Lemacik2;
     hence thesis;
   end;

WW1: {1,2,3} <> {3,4}
     proof
       set z=4;
       not z in {1,2,3} by ENUMSET1:def 1;
       hence thesis by TARSKI:def 2;
     end;

The0: {{},{1,2},{3,4},{1,2,3,4}} <> bool {1,2,3,4}
proof
  set y={1,2,3};
    not 4 in {1,2,3} by ENUMSET1:def 1; then
b1: y <> {1,2,3,4} by ENUMSET1:def 2;
    3 in {1,2,3} by ENUMSET1:def 1; then
K1: y<>{1,2} by TARSKI:def 2;
    not (y in {{},{1,2}} or y in {{3,4}})
    proof
      (not y in {{}}) & not y in {{1,2}} by K1,TARSKI:def 1; then
      not y in {{}} \/ {{1,2}} by XBOOLE_0:def 3;
      hence thesis by TARSKI:def 1,WW1,ENUMSET1:1;
    end; then
    not y in {{},{1,2}} \/ {{3,4}} by XBOOLE_0:def 3; then
    not (y in {{},{1,2},{3,4}} or y in {{1,2,3,4}})
      by b1,ENUMSET1:3,TARSKI:def 1; then
   not y in {{},{1,2},{3,4}} \/ {{1,2,3,4}} by XBOOLE_0:def 3;
  hence thesis by B123,ENUMSET1:6;
end;

set Omega3 = {1,2,3}, Omega4 = {1,2,3,4};

ATh102: {1,2,3} c< {1,2,3,4}
 proof
  for x being object st x in Omega3 holds x in Omega4
  proof
   let x be object;
   assume x in Omega3;
   then x=1 or x=2 or x=3 or x=4 by ENUMSET1:def 1;
   hence thesis by ENUMSET1:def 2;
  end; then
  T1: Omega3 c= Omega4;
  Omega3 <> Omega4
  proof
    4 in {1,2,3,4} by ENUMSET1:def 2;
    hence thesis by ENUMSET1:def 1;
  end;
  hence thesis by T1;
 end;

 set Omega2 = {1,2};

ATh101: {1,2} c< {1,2,3}
 proof
  for x being object st x in Omega2 holds x in Omega3
  proof
   let x be object;
   assume x in Omega2; then
   x = 1 or x = 2 by TARSKI:def 2;
   hence thesis by ENUMSET1:def 1;
  end; then
  T1: Omega2 c= Omega3;
  Omega2 <> Omega3
  proof
    3 in {1,2,3} by ENUMSET1:def 1;
    hence thesis by TARSKI:def 2;
  end;
  hence thesis by T1;
  end;

registration let I be non empty Subset of NAT;
  cluster In(I,bool REAL) -> non empty;
  coherence
  proof
    I c= REAL by NUMBERS:19;
    hence thesis by SUBSET_1:def 8;
  end;
end;

theorem
  for T being Nat holds
   {w where w is Element of NAT: w>0 & w<=T} c=
     {w where w is Element of NAT: w<=T}
proof
  let T be Nat;
  let x be object;
  assume x in {w where w is Element of NAT: w>0 & w<=T}; then
  consider w being Element of NAT such that B1: x=w & w>0 & w<=T;
  thus thesis by B1;
end;

theorem
  for T being Nat holds
    {w where w is Element of NAT: w <= T} is non empty Subset of NAT
proof
  let T be Nat;
  B1: {w where w is Element of NAT: w <= T} c= NAT
  proof
    let x be object;
    assume x in {w where w is Element of NAT: w <= T};
    then consider w being Element of NAT such that C1: x=w & w<=T;
   thus thesis by C1;
  end;
   T in {w where w is Element of NAT: w <= T}
   proof
    T in NAT by ORDINAL1:def 12;
    hence thesis;
   end;
  hence thesis by B1;
end;

theorem
  for T being Nat st T>0 holds
    {w where w is Element of NAT: w>0 & w <= T} is non empty Subset of NAT
proof
 let T be Nat;
 assume A0: T>0;
  B1: {w where w is Element of NAT: w>0 & w <= T} c= NAT
  proof
    let x be object;
    assume x in {w where w is Element of NAT: w>0 & w <= T};
    then consider w being Element of NAT such that C1: x=w & w>0 & w <= T;
   thus thesis by C1;
  end;
  1>0 & 1<=T
  proof
    T>0 & T=1*T by A0;
    hence thesis by NAT_1:24;
  end; then
  1 in {w where w is Element of NAT: w>0 & w <= T};
  hence thesis by B1;
end;

:: Special Random-Variables

theorem
  for d being Nat,
      phi being Real_Sequence,
      Omega being non empty set,
      F being SigmaField of Omega,
      X being non empty set,
      G being sequence of X,
      w being Element of Omega holds
   {PortfolioValueFutExt(d,phi,F,G,w)} is Event of Borel_Sets by FINANCE2:5;

definition
  let d be Nat;
  let phi be Real_Sequence;
  let Omega be non empty set;
  let F be SigmaField of Omega;
  let X be non empty set;
  let G be sequence of X;
  let w be Element of Omega;
  redefine func PortfolioValueFutExt(d,phi,F,G,w) -> Element of REAL;  :: redefines PortfolioValueFutExt (FINANCE1, definition)
  coherence;
end;

definition
  let Omega be non empty set;
  let F be SigmaField of Omega;
  let X be non empty set;
  let G be sequence of X;
  let phi be Real_Sequence;
  let d be Nat;
  func RVPortfolioValueFutExt(phi,F,G,d) -> Function of Omega,REAL
   means :Def2:
   for w being Element of Omega holds
     it.w = PortfolioValueFutExt(d,phi,F,G,w);
   existence
   proof
     deffunc U(Element of Omega) = PortfolioValueFutExt(d,phi,F,G,$1);
     consider f being Function of Omega,REAL such that
 A1: for d be Element of Omega holds f.d = U(d) from FUNCT_2:sch 4;
     take f;
     let n be Element of Omega;
     thus thesis by A1;
   end;
   uniqueness
   proof
     let f1,f2 be Function of Omega,REAL;
     assume that
 A2: for w being Element of Omega holds f1.w =
       PortfolioValueFutExt(d,phi,F,G,w) and
 A3: for w being Element of Omega holds f2.w =
       PortfolioValueFutExt(d,phi,F,G,w);
     for w being Element of Omega holds f1.w=f2.w
     proof
       let w be Element of Omega;
       f2.w = PortfolioValueFutExt(d,phi,F,G,w) by A3;
       hence thesis by A2;
     end;
     hence thesis;
   end;
end;

theorem
  for Omega be non empty set
  for F be SigmaField of Omega
  for G be sequence of set_of_random_variables_on(F,Borel_Sets)
  for phi be Real_Sequence
  for d be Nat holds
  RVPortfolioValueFutExt(phi,F,G,d) is random_variable of F,Borel_Sets
 proof
  let Omega be non empty set;
  let F be SigmaField of Omega;
  let G be sequence of set_of_random_variables_on(F,Borel_Sets);
  let phi be Real_Sequence;
  let d be Nat;
  defpred J[Nat] means RVPortfolioValueFutExt(phi,F,G,$1)
   is random_variable of F,Borel_Sets;
   ElementsOfPortfolioValueProb_fut(F,G.0) is
    random_variable of F,Borel_Sets by FINANCE2:28; then
   A1: (phi.0(#)ElementsOfPortfolioValueProb_fut(F,G.0)) is
    random_variable of F,Borel_Sets by FINANCE2:26;
  (RVPortfolioValueFutExt(phi,F,G,0)) is random_variable of F,Borel_Sets
  proof
   for w being Element of Omega holds
    (RVPortfolioValueFutExt(phi,F,G,0)).w =
     (phi.0(#)ElementsOfPortfolioValueProb_fut(F,G.0)).w
   proof
    let w be Element of Omega;
    (RVPortfolioValueFutExt(phi,F,G,0)).w = PortfolioValueFutExt(0,phi,F,G,w)
     by Def2; then
    (RVPortfolioValueFutExt(phi,F,G,0)).w =
     (RVPortfolioValueFutExt_El(phi,F,G,w)).0 by SERIES_1:def 1
     .= (RVElementsOfPortfolioValue_fut(phi,F,G,0)).w by FINANCE2:def 6
     .= phi.0 * ElementsOfPortfolioValueProb_fut(F,G.0).w by FINANCE2:def 5;
   hence thesis by VALUED_1:6;
   end;
  hence thesis by A1,FUNCT_2:63;
  end; then
  J0: J[0];
  J1: for n being Nat st J[n] holds J[n+1]
  proof
   let n be Nat;
   assume B1: J[n];
     C0: for w being Element of Omega holds
          (RVPortfolioValueFutExt(phi,F,G,(n+1))).w =
           (RVPortfolioValueFutExt(phi,F,G,n)).w +
            (RVElementsOfPortfolioValue_fut(phi,F,G,(n+1))).w
     proof
      let w be Element of Omega;
      (RVPortfolioValueFutExt(phi,F,G,(n+1))).w =
       PortfolioValueFutExt((n+1),phi,F,G,w) by Def2; then
      D1: (RVPortfolioValueFutExt(phi,F,G,(n+1))).w =
       Partial_Sums((RVPortfolioValueFutExt_El(phi,F,G,w))).n +
        (RVPortfolioValueFutExt_El(phi,F,G,w)).(n+1) by SERIES_1:def 1;
      (RVPortfolioValueFutExt(phi,F,G,n)).w = PortfolioValueFutExt(n,phi,F,G,w)
       by Def2;
     hence thesis by FINANCE2:def 6,D1;
     end;
K2:   RVElementsOfPortfolioValue_fut(phi,F,G,n+1)
      is random_variable of F,Borel_Sets by FINANCE2:30;
C2: dom (RVPortfolioValueFutExt(phi,F,G,n)) = Omega by FUNCT_2:def 1;
      dom (RVElementsOfPortfolioValue_fut(phi,F,G,(n+1))) = Omega
       by FUNCT_2:def 1; then
      dom (RVPortfolioValueFutExt(phi,F,G,(n+1))) =
      dom (RVPortfolioValueFutExt(phi,F,G,n)) /\
       dom (RVElementsOfPortfolioValue_fut(phi,F,G,(n+1))) &
     for c being object st c in dom (RVPortfolioValueFutExt(phi,F,G,(n+1)))
      holds (RVPortfolioValueFutExt(phi,F,G,(n+1))).c =
       (RVPortfolioValueFutExt(phi,F,G,n)).c +
        (RVElementsOfPortfolioValue_fut(phi,F,G,(n+1))).c
        by C0, FUNCT_2:def 1,C2;
     then (RVPortfolioValueFutExt(phi,F,G,(n+1))) =
      (RVPortfolioValueFutExt(phi,F,G,n)) +
       (RVElementsOfPortfolioValue_fut(phi,F,G,(n+1))) by VALUED_1:def 1;
     hence thesis by B1,K2,FINANCE2:23;
    end;
  for n being Nat holds J[n] from NAT_1:sch 2(J0,J1);
 hence thesis;
 end;

definition
  let d be Nat;
  let phi be Real_Sequence;
  let Omega be non empty set;
  let F be SigmaField of Omega;
  let X be non empty set;
  let G be sequence of X;
  let w be Element of Omega;
  redefine func PortfolioValueFut(d,phi,F,G,w) -> Real equals  :: redefines PortfolioValueFut (FINANCE1, definition)
  Partial_Sums((RVPortfolioValueFutExt_El(phi,F,G,w))^\1).(d-1);
 correctness
 proof
 per cases;
 suppose A0: d=0; then
 not (d-1) in dom Partial_Sums(ElementsOfPortfolioValue_fut(phi,F,w,G)^\1);
 then
 A1: Partial_Sums(ElementsOfPortfolioValue_fut(phi,F,w,G)^\1).(d-1) = {}
  by FUNCT_1:def 2;
 not (d-1) in dom Partial_Sums((RVPortfolioValueFutExt_El(phi,F,G,w))^\1)
  by A0;
 hence thesis by A1,FUNCT_1:def 2;
 end;
 suppose A0: d<>0;
  for k being Nat holds
   Partial_Sums(ElementsOfPortfolioValue_fut(phi,F,w,G)^\1).k
    = Partial_Sums((RVPortfolioValueFutExt_El(phi,F,G,w))^\1).k
  proof
   let k be Nat;
   defpred J[Nat] means
    Partial_Sums(ElementsOfPortfolioValue_fut(phi,F,w,G)^\1).$1 =
     Partial_Sums((RVPortfolioValueFutExt_El(phi,F,G,w))^\1).$1;
   consider k being Nat such that B0: k=0;
   Partial_Sums(ElementsOfPortfolioValue_fut(phi,F,w,G)^\1).k =
    (ElementsOfPortfolioValue_fut(phi,F,w,G)^\1).k by B0,SERIES_1:def 1;
    then
B1: Partial_Sums(ElementsOfPortfolioValue_fut(phi,F,w,G)^\1).k =
        (ElementsOfPortfolioValue_fut(phi,F,w,G)).(k+1) by NAT_1:def 3;
   Partial_Sums(RVPortfolioValueFutExt_El(phi,F,G,w)^\1).k =
        (RVPortfolioValueFutExt_El(phi,F,G,w)^\1).k by B0,SERIES_1:def 1
    .= (RVPortfolioValueFutExt_El(phi,F,G,w)).(k+1) by NAT_1:def 3
    .= (RVElementsOfPortfolioValue_fut(phi,F,G,k+1)).w by FINANCE2:def 6; then
   Partial_Sums(RVPortfolioValueFutExt_El(phi,F,G,w)^\1).k =
    ElementsOfPortfolioValueProb_fut(F,G.(k+1)).w * phi.(k+1)
     by FINANCE2:def 5; then
   J0: J[0] by FINANCE1:def 10, B1, B0;
   J1: for n being Nat st J[n] holds J[n+1]
   proof
    let n be Nat;
    assume C0: J[n];
      (ElementsOfPortfolioValue_fut(phi,F,w,G)^\1).(n+1) =
       (ElementsOfPortfolioValue_fut(phi,F,w,G)).((n+1)+1) by NAT_1:def 3
       .= ElementsOfPortfolioValueProb_fut(F,G.((n+1)+1)).w * phi.((n+1)+1)
        by FINANCE1:def 10
       .= RVElementsOfPortfolioValue_fut(phi,F,G,((n+1)+1)).w
        by FINANCE2:def 5
       .= RVPortfolioValueFutExt_El(phi,F,G,w).((n+1)+1) by FINANCE2:def 6;
       then (ElementsOfPortfolioValue_fut(phi,F,w,G)^\1).(n+1) =
        (RVPortfolioValueFutExt_El(phi,F,G,w)^\1).(n+1) by NAT_1:def 3;
     then
     Partial_Sums(ElementsOfPortfolioValue_fut(phi,F,w,G)^\1).(n+1) =
      Partial_Sums((RVPortfolioValueFutExt_El(phi,F,G,w))^\1).n +
       (RVPortfolioValueFutExt_El(phi,F,G,w)^\1).(n+1) by SERIES_1:def 1,C0
    .= Partial_Sums((RVPortfolioValueFutExt_El(phi,F,G,w))^\1).(n+1)
      by SERIES_1:def 1;
   hence thesis;
   end;
   for n being Nat holds J[n] from NAT_1:sch 2(J0,J1);
  hence thesis;
  end;
 hence thesis by A0;
 end;
 end;
end;

definition
  let d be Nat;
  let phi be Real_Sequence;
  let Omega be non empty set;
  let F be SigmaField of Omega;
  let X be non empty set;
  let G be sequence of X;
  let w be Element of Omega;
  redefine func PortfolioValueFut(d,phi,F,G,w) -> Element of REAL;  :: redefines PortfolioValueFut (FINANCE1, definition)
  coherence by XREAL_0:def 1;
end;

definition
  let Omega be non empty set;
  let F be SigmaField of Omega;
  let X be non empty set;
  let G be sequence of X;
  let phi be Real_Sequence;
  let d be Nat;
  func RVPortfolioValueFut(phi,F,G,d) -> Function of Omega,REAL means :Def4:
  for w being Element of Omega holds
   it.w = PortfolioValueFut(d+1,phi,F,G,w);
  existence
  proof
    deffunc U(Element of Omega) = PortfolioValueFut(d+1,phi,F,G,$1);
    consider f being Function of Omega,REAL such that
A1: for d be Element of Omega holds f.d = U(d) from FUNCT_2:sch 4;
    take f;
    let n be Element of Omega;
    thus thesis by A1;
  end;
  uniqueness
  proof
    let f1,f2 be Function of Omega,REAL;
    assume that
A2: for w being Element of Omega holds f1.w =
      PortfolioValueFut(d+1,phi,F,G,w) and
A3: for w being Element of Omega holds f2.w =
      PortfolioValueFut(d+1,phi,F,G,w);
    for w being Element of Omega holds f1.w=f2.w
    proof
      let w be Element of Omega;
      f2.w = PortfolioValueFut(d+1,phi,F,G,w) by A3;
      hence thesis by A2;
    end;
    hence thesis;
  end;
end;

theorem
  for Omega be non empty set
  for F be SigmaField of Omega
  for G be sequence of set_of_random_variables_on(F,Borel_Sets)
  for phi be Real_Sequence
  for d be Nat holds
   RVPortfolioValueFut(phi,F,G,d) is random_variable of F,Borel_Sets
 proof
  let Omega be non empty set;
  let F be SigmaField of Omega;
  let G be sequence of set_of_random_variables_on(F,Borel_Sets);
  let phi be Real_Sequence;
  let d be Nat;
  defpred J[Nat] means RVPortfolioValueFut(phi,F,G,$1)
   is random_variable of F,Borel_Sets;
   ElementsOfPortfolioValueProb_fut(F,G.(0+1)) is
    random_variable of F,Borel_Sets by FINANCE2:28; then
   A1: (phi.(0+1)(#)ElementsOfPortfolioValueProb_fut(F,G.(0+1))) is
    random_variable of F,Borel_Sets by FINANCE2:26;
  (RVPortfolioValueFut(phi,F,G,0)) is random_variable of F,Borel_Sets
  proof
   for w being Element of Omega holds
    (RVPortfolioValueFut(phi,F,G,0)).w =
     (phi.(0+1)(#)ElementsOfPortfolioValueProb_fut(F,G.(0+1))).w
   proof
    let w be Element of Omega;
    consider k being Nat such that B0: k=0;
    (RVPortfolioValueFut(phi,F,G,k)).w = PortfolioValueFut(k+1,phi,F,G,w)
     by Def4
    .= ((RVPortfolioValueFutExt_El(phi,F,G,w))^\1).k by B0,SERIES_1:def 1
    .= (RVPortfolioValueFutExt_El(phi,F,G,w)).(k+1) by NAT_1:def 3
    .= (RVElementsOfPortfolioValue_fut(phi,F,G,k+1)).w by FINANCE2:def 6;
    then (RVPortfolioValueFut(phi,F,G,0)).w
     = ElementsOfPortfolioValueProb_fut(F,G.(0+1)).w * phi.(0+1)
      by FINANCE2:def 5,B0;
   hence thesis by VALUED_1:6;
   end;
  hence thesis by A1,FUNCT_2:63;
  end;
  then
  J0: J[0];
  J1: for n being Nat st J[n] holds J[n+1]
  proof
   let n be Nat;
   assume B1: J[n];
     C0: for w being Element of Omega holds
          (RVPortfolioValueFut(phi,F,G,(n+1))).w =
           (RVPortfolioValueFut(phi,F,G,n)).w +
            (RVElementsOfPortfolioValue_fut(phi,F,G,(n+1)+1)).w
     proof
      let w be Element of Omega;
      set k=n+1;
      (RVPortfolioValueFut(phi,F,G,k)).w = PortfolioValueFut(k+1,phi,F,G,w)
       by Def4; then
      (RVPortfolioValueFut(phi,F,G,k)).w =
       PortfolioValueFut(n+1,phi,F,G,w) +
        ((RVPortfolioValueFutExt_El(phi,F,G,w))^\1).(n+1) by SERIES_1:def 1;
      then
      (RVPortfolioValueFut(phi,F,G,k)).w =
       (RVPortfolioValueFut(phi,F,G,n)).w +
        ((RVPortfolioValueFutExt_El(phi,F,G,w))^\1).(n+1) by Def4
      .= (RVPortfolioValueFut(phi,F,G,n)).w +
        ((RVPortfolioValueFutExt_El(phi,F,G,w))).((n+1)+1) by NAT_1:def 3;
     hence thesis by FINANCE2:def 6;
     end;
K1:  RVElementsOfPortfolioValue_fut(phi,F,G,n+1+1)
     is random_variable of F,Borel_Sets by FINANCE2:30;
 C2: dom (RVPortfolioValueFut(phi,F,G,n)) = Omega by FUNCT_2:def 1;
     dom (RVElementsOfPortfolioValue_fut(phi,F,G,(n+1)+1)) = Omega
       by FUNCT_2:def 1; then
     dom (RVPortfolioValueFut(phi,F,G,(n+1))) =
      dom (RVPortfolioValueFut(phi,F,G,n)) /\
       dom (RVElementsOfPortfolioValue_fut(phi,F,G,(n+1)+1)) &
     for c being object st c in dom (RVPortfolioValueFut(phi,F,G,(n+1)))
      holds (RVPortfolioValueFut(phi,F,G,(n+1))).c =
             (RVPortfolioValueFut(phi,F,G,n)).c +
              (RVElementsOfPortfolioValue_fut(phi,F,G,(n+1)+1)).c
            by C0,FUNCT_2:def 1,C2; then
      (RVPortfolioValueFut(phi,F,G,(n+1))) =
         (RVPortfolioValueFut(phi,F,G,n)) +
           (RVElementsOfPortfolioValue_fut(phi,F,G,(n+1)+1))
             by VALUED_1:def 1;
     hence thesis by B1,K1,FINANCE2:23;
  end;
  for n being Nat holds J[n] from NAT_1:sch 2(J0,J1);
 hence thesis;
 end;

theorem
  for d being Nat,
      phi be Real_Sequence,
      Omega be non empty set,
      F be SigmaField of Omega,
      X be non empty set,
      G be sequence of X,
      w be Element of Omega holds
   PortfolioValueFut(d+1,phi,F,G,w) = RVPortfolioValueFut(phi,F,G,d).w &
   {PortfolioValueFut(d+1,phi,F,G,w)} is Event of Borel_Sets
    by Def4, FINANCE2:5;

theorem
  for Omega being non empty set,
      F being SigmaField of Omega,
      X being non empty set,
      G being sequence of X,
      phi being Real_Sequence,
      d being Nat holds
  RVPortfolioValueFutExt(phi,F,G,d+1) = RVPortfolioValueFut(phi,F,G,d) +
   RVElementsOfPortfolioValue_fut(phi,F,G,0)
 proof
  let Omega be non empty set;
  let F be SigmaField of Omega;
  let X be non empty set;
  let G be sequence of X;
  let phi be Real_Sequence;
  let d be Nat;
  C0: for w being Element of Omega holds
       RVPortfolioValueFutExt(phi,F,G,d+1).w =
        RVPortfolioValueFut(phi,F,G,d).w +
         (RVElementsOfPortfolioValue_fut(phi,F,G,0)).w
  proof
   let w be Element of Omega;
   A01: RVPortfolioValueFut(phi,F,G,d).w =
    PortfolioValueFut((d+1),phi,F,G,w) by Def4;
   for d being Nat holds
    Partial_Sums((RVPortfolioValueFutExt_El(phi,F,G,w))^\1).d =
     (Partial_Sums((RVPortfolioValueFutExt_El(phi,F,G,w))).(d+1) -
      (RVPortfolioValueFutExt_El(phi,F,G,w)).0)
   proof
    defpred J[Nat] means
     Partial_Sums((RVPortfolioValueFutExt_El(phi,F,G,w))^\1).$1 =
      (Partial_Sums((RVPortfolioValueFutExt_El(phi,F,G,w))).($1+1) -
       (RVPortfolioValueFutExt_El(phi,F,G,w)).0);
     B1: Partial_Sums((RVPortfolioValueFutExt_El(phi,F,G,w))^\1).0 =
      ((RVPortfolioValueFutExt_El(phi,F,G,w))^\1).0 by SERIES_1:def 1;
    Partial_Sums((RVPortfolioValueFutExt_El(phi,F,G,w))^\1).0 =
     (Partial_Sums((RVPortfolioValueFutExt_El(phi,F,G,w))).(0+1) -
      (RVPortfolioValueFutExt_El(phi,F,G,w)).0)
    proof
     (Partial_Sums((RVPortfolioValueFutExt_El(phi,F,G,w)))).(0+1) =
      (Partial_Sums((RVPortfolioValueFutExt_El(phi,F,G,w)))).0 +
       (RVPortfolioValueFutExt_El(phi,F,G,w)).(0+1) by SERIES_1:def 1;
     then
     Partial_Sums((RVPortfolioValueFutExt_El(phi,F,G,w))^\1).0 =
      (Partial_Sums((RVPortfolioValueFutExt_El(phi,F,G,w)))).(0+1) -
       Partial_Sums(RVPortfolioValueFutExt_El(phi,F,G,w)).0 by NAT_1:def 3,B1;
    hence thesis by SERIES_1:def 1;
    end;
    then
    J0: J[0];
    J1: for n being Nat st J[n] holds J[n+1]
    proof
     let n be Nat;
     assume Q0: J[n];
     Partial_Sums((RVPortfolioValueFutExt_El(phi,F,G,w))^\1).(n+1) =
           Partial_Sums((RVPortfolioValueFutExt_El(phi,F,G,w))^\1).n +
            ((RVPortfolioValueFutExt_El(phi,F,G,w))^\1).(n+1)
       by SERIES_1:def 1
       .= ((Partial_Sums((RVPortfolioValueFutExt_El(phi,F,G,w)))).(n+1) +
        ((RVPortfolioValueFutExt_El(phi,F,G,w))^\1).(n+1) -
         (RVPortfolioValueFutExt_El(phi,F,G,w)).0) by Q0
       .= ((Partial_Sums((RVPortfolioValueFutExt_El(phi,F,G,w)))).(n+1) +
        ((RVPortfolioValueFutExt_El(phi,F,G,w))).((n+1)+1)) -
         (RVPortfolioValueFutExt_El(phi,F,G,w)).0 by NAT_1:def 3;
     hence thesis by SERIES_1:def 1;
    end;
    for n being Nat holds J[n] from NAT_1:sch 2(J0,J1);
   hence thesis;
   end;
   then
   RVPortfolioValueFut(phi,F,G,d).w =
    PortfolioValueFutExt(d+1,phi,F,G,w) -
      (RVPortfolioValueFutExt_El(phi,F,G,w)).0 by A01
    .= PortfolioValueFutExt(d+1,phi,F,G,w) -
     (RVElementsOfPortfolioValue_fut(phi,F,G,0)).w by FINANCE2:def 6;
  hence thesis by Def2;
  end;
   C2: dom (RVPortfolioValueFut(phi,F,G,d)) = Omega by FUNCT_2:def 1;
   dom (RVElementsOfPortfolioValue_fut(phi,F,G,0)) = Omega
    by FUNCT_2:def 1; then
  dom RVPortfolioValueFutExt(phi,F,G,d+1) =
   dom (RVPortfolioValueFut(phi,F,G,d)) /\
    dom (RVElementsOfPortfolioValue_fut(phi,F,G,0)) &
  for c being object st c in dom RVPortfolioValueFutExt(phi,F,G,d+1)
   holds (RVPortfolioValueFutExt(phi,F,G,d+1)).c =
    RVPortfolioValueFut(phi,F,G,d).c +
     (RVElementsOfPortfolioValue_fut(phi,F,G,0)).c
     by C0, FUNCT_2:def 1,C2;
 hence thesis by VALUED_1:def 1;
 end;

Lm1B:
   for Omega,Omega2 being non empty set,
       F being Function of Omega, Omega2,
       y being non empty set holds
   {z where z is Element of Omega: F.z is Element of y} = F"y
   proof
    let Omega,Omega2 be non empty set,
        F be Function of Omega, Omega2,
        y be non empty set;
    set D = {z where z is Element of Omega: F.z is Element of y};
    for x be object holds x in D iff x in F"y
    proof
      let x be object;
      hereby assume x in D; then
        consider z be Element of Omega such that
        A1:  x = z & F.z is Element of y;
        z in Omega; then
        z in dom F by FUNCT_2:def 1;
        hence x in F"y by FUNCT_1:def 7,A1;
      end;
      assume x in F"y; then
      x in dom F & F.x in y by FUNCT_1:def 7;
      hence x in D;
    end;
   hence thesis by TARSKI:2;
   end;

theorem 1A5:
  for Omega, Omega2 being non empty set,
      Sigma being SigmaField of Omega,
      Sigma2 being SigmaField of Omega2,
      s being Element of Omega2 holds
   Omega --> s is (Sigma,Sigma2)-random_variable-like
 proof
  let Omega, Omega2 be non empty set;
  let Sigma be SigmaField of Omega;
  let Sigma2 be SigmaField of Omega2;
  let s be Element of Omega2;
  set X = Omega --> s;
   let x be set;
   per cases;
   suppose
    A1: s in x;
    for q being object holds
     q in {w where w is Element of Omega: X.w is Element of x} iff q in Omega
    proof
     let q be object;
     hereby assume
     q in {w where w is Element of Omega: X.w is Element of x}; then
     ex w being Element of Omega st w=q & X.w is Element of x;
     hence q in Omega;
    end;
    assume q in Omega;
    then reconsider w = q as Element of Omega;
    X.w is Element of x by A1,FUNCOP_1:7;
    hence thesis;
    end; then
    {w where w is Element of Omega: X.w is Element of x}=Omega by TARSKI:2;
    then X"x = Omega by A1,Lm1B; then
    X"x is Element of Sigma by PROB_1:23;
    hence thesis;
   end;
   suppose
    A3: not s in x;
    X"x c= {}
    proof
     let q be object;
     assume q in X"x; then
     q in dom X & X.q in x by FUNCT_1:def 7;
     hence q in {} by A3,FUNCOP_1:7;
    end; then
    X"x = {}; then
    X"x is Element of Sigma by PROB_1:22;
    hence thesis;
   end;
 end;

theorem
  for Omega being non empty set,
      Sigma being SigmaField of Omega,
      RV being random_variable of Sigma,Borel_Sets,
      K being Real holds
    RV-(Omega-->K) is random_variable of Sigma,Borel_Sets
proof
  let Omega be non empty set,
      Sigma be SigmaField of Omega,
      RV be random_variable of Sigma,Borel_Sets,
      K be Real;
  reconsider KK = K as Element of REAL by XREAL_0:def 1;
  Omega-->KK is random_variable of Sigma,Borel_Sets by 1A5;
  hence thesis by FINANCE2:24;
end;

definition
  let Omega be non empty set;
  let RV be Function of Omega,REAL;
  let w be Element of Omega;
  func SetForCall-Option(RV,w) -> Element of REAL equals :Def89:
  RV.w if RV.w>=0 otherwise 0;
  correctness by NUMBERS:19;
end;

definition
  let Omega be non empty set;
  let Sigma be SigmaField of Omega;
  let RV be random_variable of Sigma,Borel_Sets;
  let K be Real;
  func Call-Option(RV,K) -> Function of Omega,REAL means
  for w being Element of Omega holds
    ((RV-(Omega-->K)).w>=0 implies it.w=(RV-(Omega-->K)).w) &
    ((RV-(Omega-->K)).w<0 implies it.w=0);
existence
proof
  reconsider MyFunc = RV-(Omega-->K) as Function of Omega,REAL;
  deffunc U(Element of Omega) = SetForCall-Option(MyFunc,$1);
     consider f being Function of Omega,REAL such that
 A1: for d be Element of Omega holds f.d = U(d) from FUNCT_2:sch 4;
  for w being Element of Omega holds
     (MyFunc.w >= 0 implies f.w=(RV-(Omega-->K)).w) &
     (MyFunc.w < 0 implies f.w = 0)
 proof
  let w be Element of Omega;
  thus MyFunc.w >= 0 implies f.w=(RV-(Omega-->K)).w
  proof
   assume B1: MyFunc.w >= 0;
   f.w = SetForCall-Option(MyFunc,w) by A1;
  hence thesis by Def89,B1;
  end;
   assume B1: MyFunc.w < 0;
   f.w = SetForCall-Option(MyFunc,w) by A1;
  hence thesis by Def89,B1;
 end;
hence thesis;
end;
uniqueness
proof
  let f1,f2 be Function of Omega,REAL;
     assume that
 A2: for w being Element of Omega holds
     ((RV-(Omega-->K)).w>=0 implies f1.w=(RV-(Omega-->K)).w) &
     ((RV-(Omega-->K)).w<0 implies f1.w=0) and
 A3: for w being Element of Omega holds
     ((RV-(Omega-->K)).w>=0 implies f2.w=(RV-(Omega-->K)).w) &
     ((RV-(Omega-->K)).w<0 implies f2.w=0);
     for w being Element of Omega holds f1.w=f2.w
     proof
       let w be Element of Omega;
       per cases;
       suppose A0: (RV-(Omega-->K)).w>=0;
         then f1.w=(RV-(Omega-->K)).w by A2;
         hence thesis by A0,A3;
       end;
       suppose A0: not (RV-(Omega-->K)).w>=0;
         then f1.w=0 by A2;
         hence thesis by A0,A3;
       end;
    end;
  hence thesis;
end;
end;

:: Special sigma-Fields

theorem SuperLemma1:
  for A1 being SetSequence of {1,2,3,4},
      w being Real st w = 1 or w = 3 holds
    (for n being Nat holds
      A1.n = {} or A1.n = {1,2} or A1.n = {3,4} or A1.n = {1,2,3,4})
  implies {w}<>Intersection A1
proof
  let A1 be SetSequence of {1,2,3,4};
  let w be Real;
  assume KX: w = 1 or w = 3;
  assume S2: for n being Nat holds
     A1.n = {} or A1.n = {1,2} or A1.n = {3,4} or A1.n = {1,2,3,4};
  per cases;
  suppose Intersection A1={};
    hence thesis;
  end;
  suppose SUPP1: Intersection A1<>{};
        ex x being object st
         (for n being Nat holds x in A1.n) & not x in {w}
        proof
         per cases;
         suppose ex j being Nat st A1.j={};
         then consider j being Nat such that J0: A1.j={};
         thus thesis by The1,J0,SUPP1;
         end;
         suppose USUPP1: for n being Nat holds A1.n<>{};
          per cases;
          suppose P1: for j being Nat holds {1,2} c= A1.j;
           set x=2;
           Z1: not x in {w} by TARSKI:def 1,KX;
           for n being Nat holds x in A1.n
           proof
            let n be Nat;
            per cases by S2;
            suppose A1.n={};
              hence thesis by USUPP1;
            end;
            suppose A1.n = {1,2};
              hence thesis by TARSKI:def 2;
            end;
            suppose J0: A1.n = {3,4};
              x in {1,2} by TARSKI:def 2; then
              not {1,2} c= A1.n by J0,TARSKI:def 2;
              hence thesis by P1;
            end;
            suppose A1.n = {1,2,3,4};
              hence thesis by ENUMSET1:def 2;
            end;
           end;
          hence thesis by Z1;
          end;
          suppose ex j being Nat st not {1,2} c= A1.j; then
           consider j being Nat such that BSUPP1: not {1,2} c= A1.j;
           per cases;
           suppose P1: for n being Nat holds {3,4} c= A1.n;
           set x=4;
           Z1: not x in {w} by TARSKI:def 1,KX;
           for n being Nat holds x in A1.n
           proof
            let n be Nat;
            per cases by S2;
            suppose A1.n={};
              hence thesis by USUPP1;
            end;
            suppose A1.n = {3,4};
              hence thesis by TARSKI:def 2;
            end;
            suppose J0: A1.n = {1,2};
              x in {3,4} by TARSKI:def 2; then
              not {3,4} c= A1.n by J0,TARSKI:def 2;
              hence thesis by P1;
            end;
            suppose A1.n = {1,2,3,4};
              hence thesis by ENUMSET1:def 2;
            end;
           end;
           hence thesis by Z1;
           end;
           suppose ex k being Nat st not {3,4} c= A1.k;
           then consider k being Nat such that CSUPP1: not {3,4} c= A1.k;
           ZW1: A1.k /\ A1.j={}
           proof
            per cases by S2,Lm2,BSUPP1;
            suppose DSUPP1: A1.j = {3,4};
              A1.k = {1,2} or A1.k = {} by S2,CSUPP1,Lm1;
              hence thesis by Lm3,DSUPP1;
            end;
            suppose A1.j = {};
              hence thesis;
            end;
           end;
           Intersection A1={}
           proof
            Intersection A1 c= A1.k /\ A1.j
            proof
             for x being object st x in Intersection A1 holds x in A1.k /\ A1.j
             proof
              let x be object;
              assume x in Intersection A1; then
              x in A1.k & x in A1.j by PROB_1:13;
             hence thesis by XBOOLE_0:def 4;
             end;
              hence thesis;
            end;
           hence thesis by ZW1;
           end;
           hence thesis by SUPP1;
           end;
          end;
         end;
      end;
     hence thesis by PROB_1:13;
    end;
end;

theorem SuperLemma2:
  for A1 being SetSequence of {1,2,3,4},
      w being Real st w = 2 or w = 4 holds
  (for n being Nat holds
     A1.n = {} or A1.n = {1,2} or A1.n = {3,4} or A1.n = {1,2,3,4})
    implies {w}<>Intersection A1
proof
  let A1 be SetSequence of {1,2,3,4};
  let w be Real;
  assume KX: w = 2 or w = 4;
  assume S2: for n being Nat holds
    A1.n = {} or A1.n = {1,2} or A1.n = {3,4} or A1.n = {1,2,3,4};
  per cases;
  suppose Intersection A1={};
    hence thesis;
  end;
  suppose SUPP1: Intersection A1<>{};
    ex x being object st (for n being Nat holds x in A1.n) & not x in {w}
    proof
      per cases;
      suppose ex j being Nat st A1.j={}; then
        consider j being Nat such that J0: A1.j={};
        thus thesis by The1,J0,SUPP1;
       end;
       suppose USUPP1: for n being Nat holds A1.n<>{};
       per cases;
       suppose P1: for j being Nat holds {1,2} c= A1.j;
         set x=1;
         Z1: not x in {w} by TARSKI:def 1,KX;
         for n being Nat holds x in A1.n
         proof
           let n be Nat;
           per cases by S2;
            suppose A1.n = {};
              hence thesis by USUPP1;
            end;
            suppose A1.n = {1,2};
              hence thesis by TARSKI:def 2;
            end;
            suppose J0: A1.n = {3,4};
              x in {1,2} by TARSKI:def 2; then
              not {1,2} c= A1.n by J0,TARSKI:def 2;
              hence thesis by P1;
            end;
            suppose A1.n = {1,2,3,4};
              hence thesis by ENUMSET1:def 2;
            end;
           end;
           hence thesis by Z1;
          end;
          suppose ex j being Nat st not {1,2} c= A1.j;
           then consider j being Nat such that BSUPP1: not {1,2} c= A1.j;
           per cases;
           suppose P1: for n being Nat holds {3,4} c= A1.n;
           set x=3;
           Z1: not x in {w} by TARSKI:def 1,KX;
           for n being Nat holds x in A1.n
           proof
            let n be Nat;
            per cases by S2;
            suppose A1.n = {};
              hence thesis by USUPP1;
            end;
            suppose A1.n = {3,4};
              hence thesis by TARSKI:def 2;
            end;
            suppose J0: A1.n = {1,2};
              x in {3,4} by TARSKI:def 2; then
              not {3,4} c= A1.n by J0,TARSKI:def 2;
              hence thesis by P1;
            end;
            suppose A1.n = {1,2,3,4};
              hence thesis by ENUMSET1:def 2;
            end;
           end;
           hence thesis by Z1;
           end;
           suppose ex k being Nat st not {3,4} c= A1.k; then
           consider k being Nat such that CSUPP1: not {3,4} c= A1.k;
           ZW1: A1.k /\ A1.j={}
           proof
            per cases by S2,Lm2,BSUPP1;
            suppose DSUPP1: A1.j = {3,4};
             per cases by CSUPP1,Lm1,S2;
             suppose A1.k={1,2};
               hence thesis by Lm3,DSUPP1;
             end;
             suppose A1.k = {};
               hence thesis;
             end;
            end;
            suppose A1.j = {};
              hence thesis;
            end;
           end;
           Intersection A1={}
           proof
            Intersection A1 c= A1.k /\ A1.j
            proof
             for x being object st x in Intersection A1 holds x in A1.k /\ A1.j
             proof
              let x be object;
              assume x in Intersection A1;
              then x in A1.k & x in A1.j by PROB_1:13;
              hence thesis by XBOOLE_0:def 4;
             end;
             hence thesis;
            end;
            hence thesis by ZW1;
           end;
           hence thesis by SUPP1;
           end;
          end;
         end;
       end;
     hence thesis by PROB_1:13;
end;
end;

theorem
  for MySigmaField, A1, A2 being set st
    MySigmaField={{},{1,2,3,4}} & A1 in MySigmaField & A2 in MySigmaField
      holds
   A1 /\ A2 in MySigmaField
proof
  let MySigmaField,A1,A2 be set;
  assume A0: MySigmaField={{},{1,2,3,4}} &
    A1 in MySigmaField & A2 in MySigmaField; then
  (A1 = {} or A1 = {1,2,3,4}) & (A2 = {} or A2 = {1,2,3,4}) by TARSKI:def 2;
  hence thesis by A0;
end;

theorem Lm700000:
  for A1 being SetSequence of {1,2,3,4} st
  (for n being Nat,k being Nat holds not (A1.n /\ A1.k = {})) &
  rng A1 c= {{},{1,2},{3,4},{1,2,3,4}} holds
  (Intersection A1 = {} or
   Intersection A1 = {1,2} or Intersection A1 = {3,4} or
   Intersection A1 = {1,2,3,4})
proof
 let A1 be SetSequence of {1,2,3,4};
 assume GENASS0: (for n being Nat,k being Nat holds not A1.n /\ A1.k = {}) &
 rng A1 c= {{},{1,2},{3,4},{1,2,3,4}};
 set MyOmega={{},{1,2},{3,4},{1,2,3,4}};
 D1: dom A1=NAT by FUNCT_2:def 1;
 S20: for n being Nat holds A1.n in {{},{1,2},{3,4},{1,2,3,4}}
 proof
   let n be Nat;
   n in dom A1 by D1,ORDINAL1:def 12;
   hence thesis by FUNCT_1:3,GENASS0;
 end;
 S2: for n being Nat holds
     A1.n = {} or A1.n = {1,2} or A1.n = {3,4} or A1.n = {1,2,3,4}
 proof
  let n be Nat;
  A1.n in {{},{1,2},{3,4},{1,2,3,4}} by S20;
  hence thesis by ENUMSET1:def 2;
 end;
 Fin1: for n being Nat holds Intersection A1 c= A1.n by PROB_1:13;
   per cases;
   suppose Intersection A1 = {1,2,3,4};
     hence thesis;
   end;
   suppose MYSUPP0: Intersection A1 <> {1,2,3,4};
   W0: Intersection A1 c= {} or Intersection A1 c= {1,2} or
   Intersection A1 c= {3,4}
   proof
    Intersection A1 = {} or Intersection A1 = {1,2} or
    Intersection A1 = {3,4}
    proof
     per cases;
     suppose ASS1: for n being Nat holds A1.n={1,2,3,4};
      Intersection A1 = {1,2,3,4}
      proof
       for x being object holds
        x in Intersection A1 iff x in {1,2,3,4}
       proof
        let x be object;
        (for n being Nat holds x in A1.n) iff x in {1,2,3,4}
        proof
         (for n being Nat holds x in A1.n) implies x in {1,2,3,4}
         proof
          assume for n being Nat holds x in A1.n; then
          x in A1.0; then
          consider k being Nat such that N10: x in A1.k;
          thus thesis by N10;
         end;
         hence thesis by ASS1;
        end;
       hence thesis by PROB_1:13;
       end;
      hence thesis by TARSKI:2;
      end;
     hence thesis by MYSUPP0;
     end;
     suppose ex n being Nat st A1.n <> {1,2,3,4}; then
      consider n being Nat such that KK: A1.n <> {1,2,3,4};
      per cases by S2;
      suppose A1.n = {};
      hence thesis by The1;
      end;
      suppose JSUPP1: A1.n = {1,2};
  Intersection A1 = {} or Intersection A1 = {1,2}
  proof
   per cases;
   suppose Intersection A1 = {1,2};
     hence thesis;
   end;
   suppose Intersection A1 <> {1,2}; then
    Intersection A1 = {1} or Intersection A1 = {2} or Intersection A1 = {}
      by ZFMISC_1:36,JSUPP1,Fin1;
    hence thesis by SuperLemma2,SuperLemma1,S2;
   end;
  end;
  hence thesis;
    end;
    suppose SUPP1: A1.n = {3,4};
  Intersection A1 = {} or Intersection A1 = {3,4}
  proof
   per cases;
   suppose Intersection A1 = {3,4};
     hence thesis;
   end;
   suppose Intersection A1 <> {3,4}; then
    Intersection A1 = {3} or Intersection A1 = {4} or Intersection A1 = {}
      by SUPP1,Fin1,ZFMISC_1:36;
    hence thesis by SuperLemma1,S2,SuperLemma2;
   end;
  end;
  hence thesis;
      end;
      suppose A1.n = {1,2,3,4};
        hence thesis by KK;
      end;
     end;
    end;
   hence thesis;
   end;
   per cases by W0;
   suppose Intersection A1 c= {};
     hence thesis;
   end;
   suppose ZW10: Intersection A1 c= {1,2};
   per cases;
   suppose Intersection A1 = {1,2};
     hence thesis;
   end;
   suppose Intersection A1 <> {1,2}; then
    Intersection A1 = {1} or Intersection A1 = {2} or Intersection A1 = {}
      by ZW10,ZFMISC_1:36;
    hence thesis by SuperLemma1,S2,SuperLemma2;
   end;
   end;
   suppose ZW10: Intersection A1 c= {3,4};
   per cases;
   suppose Intersection A1={3,4};
     hence thesis;
   end;
   suppose Intersection A1 <> {3,4}; then
    Intersection A1 = {3} or Intersection A1 = {4} or Intersection A1 = {}
      by ZW10,ZFMISC_1:36;
    hence thesis by SuperLemma1,S2,SuperLemma2;
   end;
   end;
   end;
end;

theorem
  for A1 being SetSequence of {1,2,3,4},
      MyOmega being set st
   MyOmega = {{},{1,2},{3,4},{1,2,3,4}} & Intersection A1={1,2,3,4} holds
   Intersection A1 in MyOmega by ENUMSET1:def 2;

theorem
  for A1 being SetSequence of {1,2,3,4},
      MyOmega being set st
   MyOmega = {{},{1,2},{3,4},{1,2,3,4}} & Intersection A1={3,4} holds
   Intersection A1 in MyOmega by ENUMSET1:def 2;

theorem
  for A1 being SetSequence of {1,2,3,4},
      MyOmega being set st
   MyOmega = {{},{1,2},{3,4},{1,2,3,4}} & Intersection A1={1,2} holds
   Intersection A1 in MyOmega by ENUMSET1:def 2;

theorem
  for A1 being SetSequence of {1,2,3,4},
      MyOmega being set st
   MyOmega = {{},{1,2},{3,4},{1,2,3,4}} & Intersection A1={} holds
   Intersection A1 in MyOmega by ENUMSET1:def 2;

theorem Lm8:
  for MyOmega being set,
      A1 being SetSequence of {1,2,3,4} st
     rng A1 c= MyOmega &
     MyOmega = {{},{1,2},{3,4},{1,2,3,4}}
  holds Intersection A1 in MyOmega
 proof
  let MyOmega be set;
  let A1 be SetSequence of {1,2,3,4};
  assume A0: rng A1 c= MyOmega & MyOmega = {{},{1,2},{3,4},{1,2,3,4}};
   Intersection A1 in {{},{1,2},{3,4},{1,2,3,4}}
   proof
    per cases;
    suppose CASE000: ex n being Nat,k being Nat st A1.n /\ A1.k = {};
    CASE0: ex n being Nat,k being Nat st A1.n misses A1.k
    proof
     consider n being Nat,k being Nat such that
      BCASE0: A1.n /\ A1.k = {} by CASE000;
      A1.n misses A1.k by BCASE0;
      hence thesis;
    end;
    CASE1: for y being object holds
     (for n being Nat,k being Nat holds y in A1.k & y in A1.n) iff y in {}
    proof
     let y be object;
     (for n being Nat,k being Nat holds y in A1.k & y in A1.n) implies
         y in {}
     proof
      assume G1: for n being Nat,k being Nat holds y in A1.k & y in A1.n;
      ex n being Nat,k being Nat st y in A1.k & y in A1.n & y in {}
      proof
       consider n being Nat,k being Nat such that
        H1: A1.n misses A1.k by CASE0;
       (y in A1.k & y in A1.n) iff y in {} by H1,XBOOLE_0:3;
      hence thesis by G1;
      end;
     hence thesis;
     end;
    hence thesis;
    end;
    Intersection A1 c= {}
    proof
     let y be object;
     y in Intersection A1 iff
      (for n being Nat,k being Nat holds y in A1.k & y in A1.n) by PROB_1:13;
     hence thesis by CASE1;
    end; then
    Intersection A1={};
    hence thesis by ENUMSET1:def 2;
    end;
    suppose CASE0: not ex n being Nat,k being Nat st A1.n /\ A1.k = {};
    Intersection A1 in {{},{1,2},{3,4},{1,2,3,4}}
     proof
      Intersection A1 = {} or
       Intersection A1 = {1,2} or Intersection A1 = {3,4} or
       Intersection A1 = {1,2,3,4} by CASE0,A0,Lm700000;
      hence thesis by ENUMSET1:def 2;
     end;
   hence thesis;
  end;
 end;
 hence thesis by A0;
end;

theorem Lm9:
  for MySigmaField, MySet being set,
      A1 being SetSequence of MySet st MySet={1,2,3,4} &
    rng A1 c= MySigmaField & MySigmaField = {{},{1,2,3,4}} holds
  Intersection A1 <> {} implies Intersection A1 in MySigmaField
proof
 let MySigmaField, MySet be set;
 let A1 be SetSequence of MySet;
 assume A0: MySet = {1,2,3,4} &
        rng A1 c= MySigmaField & MySigmaField = {{},{1,2,3,4}};
 assume A5: Intersection A1 <> {};
 D1: dom A1=NAT by FUNCT_2:def 1;
 A4: for n being Nat holds A1.n={} or A1.n={1,2,3,4}
 proof
  let n be Nat;
   A1.n in MySigmaField
   proof
    n in dom A1 by D1,ORDINAL1:def 12;
   hence thesis by FUNCT_1:3, A0;
  end;
 hence thesis by A0,TARSKI:def 2;
 end;
   H1: (ex n being Nat st A1.n={}) implies Intersection A1={}
   proof
     assume ex n being Nat st A1.n={}; then
     for x being object holds x in Intersection A1 iff x in {}
       by PROB_1:13;
     hence thesis by TARSKI:def 3;
   end;
   Intersection A1 = {1,2,3,4}
   proof
      for x being object holds
       x in Intersection A1 iff x in {1,2,3,4}
      proof
       let x be object;
       x in Intersection A1 iff for n being Nat holds x in {1,2,3,4}
       proof
        thus x in Intersection A1 implies
             for n being Nat holds x in {1,2,3,4}
        proof
         assume G1: x in Intersection A1;
         for n being Nat holds x in {1,2,3,4}
         proof
          let n be Nat;
          for x being object holds x in A1.n iff x in {1,2,3,4} by H1,A4,A5;
         hence thesis by PROB_1:13,G1;
         end;
        hence thesis;
        end;
         assume G1: for n being Nat holds x in {1,2,3,4};
         for n being Nat holds x in A1.n
         proof
          let n be Nat;
          x in {1,2,3,4} by G1;
          hence thesis by H1,A4,A5;
         end;
        hence thesis by PROB_1:13;
       end;
      hence thesis;
      end;
   hence thesis by TARSKI:def 3;
   end;
  hence thesis by A0,TARSKI:def 2;
end;

theorem
  for MySigmaField, MySet being set,
      A1 being SetSequence of MySet st
    MySet={1,2,3,4} &
    rng A1 c= MySigmaField & MySigmaField = {{},{1,2,3,4}} holds
  for k1 being Nat, k2 being Nat holds A1.k1 /\ A1.k2 in MySigmaField
proof
  let MySigmaField, MySet be set;
  let A1 be SetSequence of MySet;
  assume A0: MySet={1,2,3,4} &
        rng A1 c= MySigmaField & MySigmaField = {{},{1,2,3,4}};
  let k1,k2 be Nat;
  D1: dom A1=NAT by FUNCT_2:def 1; then
   k1 in dom A1 by ORDINAL1:def 12; then
  B1: A1.k1 in MySigmaField by FUNCT_1:3, A0;
   k2 in dom A1 by D1,ORDINAL1:def 12; then
  B2: A1.k2 in MySigmaField by FUNCT_1:3,A0;
  A1.k1 /\ A1.k2 in MySigmaField
  proof
    (A1.k1 = {} or A1.k1 = {1,2,3,4}) &
      (A1.k2 = {} or A1.k2 = {1,2,3,4}) by B2,B1,A0,TARSKI:def 2;
    hence thesis by A0,TARSKI:def 2;
  end;
  hence thesis;
 end;

definition
  func Special_SigmaField1 -> SigmaField of {1,2,3,4} equals
    {{},{1,2,3,4}};  ::: it is "trivial" SigmaField cobool ({{},X}) from TEX_1
correctness
proof
  set MySigmaField = {{},{1,2,3,4}};
  set ThisSigma=bool {1,2,3,4};
   MySigmaField c= bool {1,2,3,4}
  proof
    let x be object;
    assume a1: x in MySigmaField;
    x = {} or x = {1,2,3,4} by a1,TARSKI:def 2;
    hence thesis by PROB_1:4,5;
   end; then
 reconsider MySigmaField as Subset-Family of {1,2,3,4};
 A1: MySigmaField is compl-closed
 proof
  for A being Subset of {1,2,3,4} st
   A in MySigmaField holds A` in MySigmaField
  proof
   let A be Subset of {1,2,3,4};
   assume A in MySigmaField; then
   per cases by TARSKI:def 2;
   suppose A = {};
   hence thesis by TARSKI:def 2;
   end;
   suppose B1: A = {1,2,3,4};
   A`={} by B1,XBOOLE_1:37;
   hence thesis by TARSKI:def 2;
 end;
 end;
 hence thesis;
 end;
 MySigmaField is sigma-multiplicative
 proof
  for A1 being SetSequence of {1,2,3,4} st rng A1 c= MySigmaField
   holds Intersection A1 in MySigmaField
  proof
   let A1 be SetSequence of {1,2,3,4};
   assume B1: rng A1 c= MySigmaField;
   per cases;
   suppose Intersection A1 = {};
   hence thesis by TARSKI:def 2;
   end;
   suppose Intersection A1 <> {};
   hence thesis by B1,Lm9;
   end;
  end;
 hence thesis;
 end;
hence thesis by A1;
end;
end;

definition
  func Special_SigmaField2 -> SigmaField of {1,2,3,4} equals
    {{},{1,2},{3,4},{1,2,3,4}};
correctness
proof
 set MyOmega = {{},{1,2},{3,4},{1,2,3,4}};
 MyOmega is Subset-Family of {1,2,3,4}
 proof
   for x being object st x in MyOmega holds x in bool {1,2,3,4}
   proof
    let x be object;
    assume x in MyOmega; then
    per cases by ENUMSET1:def 2;
    suppose x = {};
     hence thesis by PROB_1:4;
    end;
    suppose x = {1,2};
      hence thesis by Lm2;
    end;
    suppose x = {3,4};
      hence thesis by Lm1;
    end;
    suppose x = {1,2,3,4};
    hence thesis by ZFMISC_1:def 1;
    end;
   end;
  hence thesis by TARSKI:def 3;
 end; then
 reconsider MyOmega as Subset-Family of {1,2,3,4};
 A1: MyOmega is compl-closed
 proof
  for A being Subset of {1,2,3,4} st A in MyOmega holds A` in MyOmega
  proof
   let A be Subset of {1,2,3,4};
   assume A in MyOmega;
   then per cases by ENUMSET1:def 2;
   suppose A = {};
   hence thesis by ENUMSET1:def 2;
   end;
   suppose A = {1,2};
    hence thesis by Lem1,ENUMSET1:def 2;
   end;
   suppose A = {3,4};
    hence thesis by Lem2,ENUMSET1:def 2;
   end;
   suppose B300: A = {1,2,3,4};
   A`={}
   proof
    reconsider B = {} as Subset of {1,2,3,4} by SUBSET_1:1;
    A=B` by B300;
    hence thesis;
   end;
   hence thesis by ENUMSET1:def 2;
   end;
  end;
 hence thesis;
 end;
 MyOmega is sigma-multiplicative by Lm8;
 hence thesis by A1;
end;
end;

definition
::$CD
end;

theorem
  for Omega being set st Omega = {1,2,3,4} holds
    {1} c= Omega &
    {2} c= Omega &
    {3} c= Omega &
    {4} c= Omega &
    {1,2} c= Omega &
    {3,4} c= Omega &
    {} c= Omega &
    Omega c= Omega
proof
  let Omega be set;
  assume A0: Omega={1,2,3,4}; then
  1 in Omega & 2 in Omega & 3 in Omega & 4 in Omega by ENUMSET1:def 2;
  hence thesis by A0,Lemacik2,ZFMISC_1:31;
end;

theorem
  for Omega being set st
    Omega={1,2,3,4} holds
    Omega in Special_SigmaField1 &
    {} in Special_SigmaField1 &
    {1,2} in Special_SigmaField2 &
    {3,4} in Special_SigmaField2 &
    Omega in Special_SigmaField2 &
    {} in Special_SigmaField2 &
    Omega in Trivial-SigmaField {1,2,3,4} &
    {} in Trivial-SigmaField {1,2,3,4} &
    {1} in Trivial-SigmaField {1,2,3,4} &
    {2} in Trivial-SigmaField {1,2,3,4} &
    {3} in Trivial-SigmaField {1,2,3,4} &
    {4} in Trivial-SigmaField {1,2,3,4}
    by EnLm1,EnLm2,EnLm3,PROB_1:5,EnLm4,PROB_1:4,ENUMSET1:def 2;

XX1: {{},{1,2,3,4}} c< {{},{1,2},{3,4},{1,2,3,4}}
   proof
    {{},{1,2,3,4}} c= {{},{1,2,3,4}} \/ {{1,2}} by XBOOLE_0:def 3;
    then {{},{1,2,3,4}} c= {{},{1,2,3,4},{1,2}} by ENUMSET1:3;
    then {{},{1,2,3,4}} c= {{},{1,2,3,4},{1,2}} \/ {{3,4}}
     by XBOOLE_0:def 3; then
    Zw1: {{},{1,2,3,4}} c= {{},{1,2,3,4},{1,2},{3,4}} by ENUMSET1:6;
   T1: {{},{1,2,3,4}} c= {{},{1,2},{3,4},{1,2,3,4}}
   proof
    for x being object st
     x in {{},{1,2,3,4}} holds x in {{},{1,2},{3,4},{1,2,3,4}}
    proof
     let x be object;
     assume ASS1: x in {{},{1,2,3,4}};
     x={} or x={1,2,3,4} or x={1,2} or x={3,4} by ASS1,Zw1,ENUMSET1:def 2;
     hence thesis by ENUMSET1:def 2;
    end;
   hence thesis;
   end;
   set y ={1,2};
   C1: y in {{},{1,2},{3,4},{1,2,3,4}} by ENUMSET1:def 2;
   {1,2} <> {1,2,3,4}
   proof
     3 in {1,2,3,4} & not 3 in {1,2} by ENUMSET1:def 2,TARSKI:def 2;
     hence thesis;
   end;
   hence thesis by T1,C1,TARSKI:def 2;
  end;

XX2: {{},{1,2},{3,4},{1,2,3,4}} c< bool {1,2,3,4}
  proof
   A2: {{1,2,3,4}} c= bool {1,2,3,4} by ZFMISC_1:68;
    {{},{1,2},{3,4},{1,2,3,4}} c= bool {1,2,3,4}
    proof
     set MyBool=bool {1,2,3,4};
     reconsider MyBool as SigmaField of {1,2,3,4};
     for x being object st x in {{},{1,2},{3,4},{1,2,3,4}}
      holds x in bool {1,2,3,4}
     proof
      let x be object;
      assume x in {{},{1,2},{3,4},{1,2,3,4}};
      then per cases by ENUMSET1:def 2;
      suppose x={}; hence thesis by PROB_1:4; end;
      suppose x={1,2};
        hence thesis by B25;
      end;
      suppose x={3,4};
        hence thesis by B26;
      end;
      suppose x={1,2,3,4}; then
        x in {{1,2,3,4}} by TARSKI:def 1;
        hence thesis by A2;
      end;
     end;
   hence thesis;
   end;
 hence thesis by The0;
 end;

theorem
  Special_SigmaField1 c< Special_SigmaField2 &
  Special_SigmaField2 c< Trivial-SigmaField {1,2,3,4} by XX1,XX2;

:: Construction of Filtration and Examples

theorem
  ex Omega being non empty set st
    ex F1,F2,F3 being SigmaField of Omega st
    F1 c< F2 & F2 c< F3
proof
  Special_SigmaField1 c< Special_SigmaField2 by XX1;
  hence thesis by XX2;
end;

theorem
  ex Omega1,Omega2,Omega3,Omega4 being non empty set st
 Omega1 c< Omega2 & Omega2 c< Omega3 & Omega3 c< Omega4 &
 (ex F1 being SigmaField of Omega1,
    F2 being SigmaField of Omega2,
    F3 being SigmaField of Omega3,
    F4 being SigmaField of Omega4 st
 F1 c= F2 & F2 c= F3 & F3 c= F4)
proof
 set Omega1={1};
 set Omega2={1,2};
 set Omega3={1,2,3};
 set Omega4={1,2,3,4};
 reconsider F1 = bool Omega1 as SigmaField of Omega1;
 reconsider F2 = bool Omega2 as SigmaField of Omega2;
 reconsider F3 = bool Omega3 as SigmaField of Omega3;
 reconsider F4 = bool Omega4 as SigmaField of Omega4;
 ATh100: Omega1 c< Omega2 by ZFMISC_1:7,20;
 E10: F1 c= F2 by ZFMISC_1:7,ZFMISC_1:67;
 E11: F2 c= F3 by ATh101,ZFMISC_1:67;
 F3 c= F4 by ATh102,ZFMISC_1:67;
 hence thesis by ATh100,ATh101,ATh102,E10,E11;
end;

definition
  let Omega be non empty set;
  let Sigma be SigmaField of Omega;
  let I be non empty real-membered set;
  mode Filtration of I,Sigma -> ManySortedSigmaField of I,Sigma means:Def2000:
  for s,t being Element of I st s<=t holds it.s is Subset of it.t;
existence
proof
  set C=Sigma;
  A1: {Sigma} c= bool Sigma by ZFMISC_1:68;
  C is Element of bool Sigma
  proof
   Sigma in {Sigma} by TARSKI:def 1;
   hence thesis by A1;
  end;
  then reconsider C as Element of bool Sigma;
  set const = I-->C;
  reconsider const as Function of I,bool Sigma;
  Z1: for i being set st i in I holds const.i is SigmaField of Omega
   by FUNCOP_1:7;
T1: const is ManySortedSigmaField of I,Sigma by Z1,KOLMOG01:def 2;
   for x,y being Element of I st x<=y holds const.x is Subset of const.y
   proof
     let x,y be Element of I;
     assume x<=y;
     const.x = C & const.y = C by FUNCOP_1:7;
     hence thesis;
   end;
   hence thesis by T1;
 end;
end;

definition
  let I, Omega be non empty set;
  let Sigma be SigmaField of Omega;
  let Filt be ManySortedSigmaField of I, Sigma;
  let i be Element of I;
  func El_Filtration(i,Filt) -> SigmaField of Omega equals
    Filt.i;
  correctness by KOLMOG01:def 2;
end;

definition
  let k be Element of {1,2,3};
  func Set1_of_SigmaField3(k) -> Subset of bool {1,2,3,4} equals :Def8:
  Special_SigmaField1 if k=1 otherwise
    Special_SigmaField2;
  correctness;
end;

definition
  let k be Element of {1,2,3};
  func Set2_of_SigmaField3(k) -> Subset of bool {1,2,3,4} equals :Def9:
  Set1_of_SigmaField3(k) if k<=2 otherwise
    Trivial-SigmaField {1,2,3,4};
  correctness;
end;

Th3:
  for Sigma being SigmaField of {1,2,3,4},
      I being set st I={1,2,3} & Sigma=bool{1,2,3,4} holds
     ex MyFunc being ManySortedSigmaField of I,Sigma st
       MyFunc.1=Special_SigmaField1 &
       MyFunc.2=Special_SigmaField2 &
       MyFunc.3=Trivial-SigmaField {1,2,3,4}
 proof
  let Sigma be SigmaField of {1,2,3,4};
  let I be set;
  assume ASS2: I={1,2,3} & Sigma=bool {1,2,3,4};
  deffunc U(Element of {1,2,3})=Set2_of_SigmaField3($1);
  consider fI1 being Function of {1,2,3},bool bool {1,2,3,4} such that
   A1: for d be Element of {1,2,3} holds fI1.d = U(d) from FUNCT_2:sch 4;
  reconsider fI1 as Function of I,bool Sigma by ASS2;
  reconsider El1 = 1 as Element of {1,2,3} by ENUMSET1:def 1;
  A20: fI1.1=Set2_of_SigmaField3(El1) by A1;
  F1: Set2_of_SigmaField3(El1)=Set1_of_SigmaField3(El1) by Def9;
  reconsider El1 = 2 as Element of {1,2,3} by ENUMSET1:def 1;
  A200: fI1.2=Set2_of_SigmaField3(El1) by A1;
  F2: Set2_of_SigmaField3(El1)=Set1_of_SigmaField3(El1) by Def9;
  reconsider El1 = 3 as Element of {1,2,3} by ENUMSET1:def 1;
  A2: fI1.3=Set2_of_SigmaField3(El1) by A1;
  reconsider fI1 as Function of I,bool Sigma;
  for i being set st i in I holds fI1.i is SigmaField of {1,2,3,4}
  proof
   let i be set;
   assume B1: i in I;
    fI1.i is SigmaField of {1,2,3,4}
    proof
     per cases by B1,ASS2,ENUMSET1:def 1;
     suppose i=1;
       hence thesis by F1,Def8, A20;
     end;
     suppose i=2;
       hence thesis by F2,Def8,A200;
     end;
     suppose i=3;
       hence thesis by Def9, A2;
     end;
    end;
   hence thesis;
  end; then
  reconsider fI1 as ManySortedSigmaField of I,Sigma by KOLMOG01:def 2;
  take fI1;
 thus thesis by F1, Def8, A20, F2,A200,Def9,A2;
 end;

theorem MyNeed:
  for Omega being non empty set,
      Sigma being SigmaField of Omega,
      I being non empty real-membered set st
      I={1,2,3} & Sigma=bool {1,2,3,4} & Omega = {1,2,3,4} holds
  ex MyFunc being Filtration of I,Sigma st
     MyFunc.1=Special_SigmaField1 &
     MyFunc.2=Special_SigmaField2 &
     MyFunc.3=Trivial-SigmaField {1,2,3,4}
 proof
  let Omega be non empty set;
  let Sigma be SigmaField of Omega;
  let I be non empty real-membered set;
  assume A0: I={1,2,3} & Sigma=bool {1,2,3,4} & Omega={1,2,3,4};
  consider MyFunc be ManySortedSigmaField of I,Sigma such that A1:
     MyFunc.1=Special_SigmaField1 &
     MyFunc.2=Special_SigmaField2 &
     MyFunc.3=Trivial-SigmaField {1,2,3,4} by A0,Th3;
  A3: for s,t being Element of I st s<=t holds MyFunc.s is Subset of MyFunc.t
  proof
   let s,t be Element of I;
   assume B1: s<=t;
   per cases by A0,ENUMSET1:def 1;
   suppose SUPP1: s=1;
    per cases by A0,ENUMSET1:def 1;
    suppose t=1; then
    MyFunc.t=MyFunc.1 & MyFunc.s=MyFunc.1 by SUPP1;
    hence thesis;
    end;
    suppose t=2 or t = 3;
    hence thesis by SUPP1,A1,XX1;
    end;
   end;
   suppose SUPP1: s=2;
    per cases by A0,ENUMSET1:def 1;
    suppose t=1;
    hence thesis by SUPP1,B1;
    end;
    suppose t=2; then
    MyFunc.t=MyFunc.2 & MyFunc.s=MyFunc.2 by SUPP1;
    hence thesis;
    end;
    suppose t=3;
    hence thesis by SUPP1,A1;
    end;
   end;
   suppose SUPP1: s=3;
    per cases by A0,ENUMSET1:def 1;
    suppose t=1 or t = 2;
      hence thesis by SUPP1,B1;
    end;
    suppose t=3; then
      MyFunc.t=MyFunc.3 & MyFunc.s=MyFunc.3 by SUPP1;
      hence thesis;
    end;
   end;
  end;
  MyFunc is Filtration of I,Sigma by A3, Def2000;
  hence thesis by A1;
 end;

Lm1A:
  for Omega, Omega2 be non empty set,
      F be Function of Omega, Omega2,
      y be non empty set holds
  {z where z is Element of Omega: F.z is Element of y} = F"y
  proof
   let Omega, Omega2 be non empty set,
       F be Function of Omega, Omega2,
       y be non empty set;
   set D = {z where z is Element of Omega: F.z is Element of y};
   for x be object holds x in D iff x in F"y
   proof
    let x be object;
    hereby assume x in D; then
    consider z be Element of Omega such that
     A1: x = z & F.z is Element of y;
     z in Omega; then
     z in dom F by FUNCT_2:def 1;
    hence x in F"y by A1,FUNCT_1:def 7;
   end;
   assume x in F"y; then
   x in dom F & F.x in y by FUNCT_1:def 7;
   hence x in D;
   end;
  hence thesis by TARSKI:2;
  end;

Lm2A: for Omega being non empty set,
          Sigma4 being SigmaField of Omega,
          Sigma5 being SigmaField of {1} holds
   Omega --> 1 is random_variable of Sigma4,Sigma5
  proof
   let Omega be non empty set;
   let Sigma4 be SigmaField of Omega;
   let Sigma5 be SigmaField of {1};
   set 1REAL=1;
   reconsider 1REAL as Real;
   reconsider X = Omega --> 1REAL as Function of Omega,{1};
   X is (Sigma4,Sigma5)-random_variable-like
   proof
    let x be set;
    per cases;
    suppose
    A1: 1 in x;
    for q being object holds
       q in {w where w is Element of Omega: X.w is Element of x} iff q in Omega
    proof
     let q be object;
     hereby assume
       q in {w where w is Element of Omega: X.w is Element of x}; then
       ex w being Element of Omega st w=q & X.w is Element of x;
       hence q in Omega;
     end;
     assume q in Omega;
     then reconsider w = q as Element of Omega;
     X.w is Element of x by A1,FUNCOP_1:7;
     hence thesis;
    end; then
    A2: {w where w is Element of Omega: X.w is Element of x}=Omega by TARSKI:2;
     {w where w is Element of Omega: X.w is Element of x}=X"x by A1,Lm1A;
     then X"x is Element of Sigma4 by A2,PROB_1:23;
    hence thesis;
    end;
    suppose
    A3: not 1 in x;
     X"x c= {}
    proof
     let q be object;
     assume q in X"x; then
     q in dom X & X.q in x by FUNCT_1:def 7;
    hence q in {} by A3,FUNCOP_1:7;
   end;
   then X"x = {}; then
   X"x is Element of Sigma4 by PROB_1:22;
   hence thesis;
   end;
   end;
  hence thesis;
  end;

theorem THJ1:
  for Omega being non empty set,
    Sigma being SigmaField of Omega,
    Sigma2 being SigmaField of {1} st
    Omega={1,2,3,4} holds
    ex X1 being Function of Omega,{1} st
     X1 is random_variable of Special_SigmaField1,Sigma2 &
     X1 is random_variable of Special_SigmaField2,Sigma2 &
     X1 is random_variable of Trivial-SigmaField {1,2,3,4},Sigma2
 proof
  let Omega be non empty set;
  let Sigma be SigmaField of Omega;
  let Sigma2 be SigmaField of {1};
  assume A1: Omega={1,2,3,4};
  reconsider 1REAL = 1 as Real;
  consider X1 being Function of Omega,{1REAL} such that F4: X1=Omega-->1REAL;
  reconsider X1 as Function of Omega,{1};
  take X1;
  thus thesis by A1,Lm2A,F4;
 end;

::  The first example of the existence of a random-variable depends
::  on a special underlying sigma-field and given Filtration

theorem
  ex Omega, Omega2 be non empty set,
     Sigma be SigmaField of Omega,
     Sigma2 be SigmaField of Omega2,
     I be non empty real-membered set,
     Q be Filtration of I,Sigma st
  ex rv being Function of Omega,Omega2 st
    for i being Element of I holds
      rv is random_variable of El_Filtration(i,Q),Sigma2
proof
  set Omega={1,2,3,4};
  set Omega2={1};
  consider Sigma being SigmaField of Omega such that A3: Sigma=bool(Omega);
  reconsider Sigma2=bool(Omega2) as non empty set;
  reconsider Sigma2 as SigmaField of Omega2;
  consider I being non empty real-membered set such that A5: I={1,2,3};
  consider MyFunc being Filtration of I,Sigma such that
  A6: MyFunc.1=Special_SigmaField1 &
      MyFunc.2=Special_SigmaField2 &
      MyFunc.3=Trivial-SigmaField {1,2,3,4} by A3,A5,MyNeed;
  consider X1 being Function of Omega,{1} such that
  A7:X1 is random_variable of Special_SigmaField1,Sigma2 &
     X1 is random_variable of Special_SigmaField2,Sigma2 &
     X1 is random_variable of Trivial-SigmaField {1,2,3,4},Sigma2 by THJ1;
  F2: for i being Element of I holds
   X1 is random_variable of El_Filtration(i,MyFunc),Sigma2
   proof
    let i be Element of I;
    i = 1 or i = 2 or i = 3 by A5,ENUMSET1:def 1;
    hence thesis by A6,A7;
   end;
  take Omega, Omega2, Sigma, Sigma2;
  thus thesis by F2;
 end;

:: Next theorem gives also the existence of random_variables
:: depending on arbitrary sigma-fields and filtrations

theorem
  for Omega, Omega2 being non empty set,
      Sigma being SigmaField of Omega,
      Sigma2 being SigmaField of Omega2,
      I being non empty real-membered set,
      Q being ManySortedSigmaField of I,Sigma holds
  ex rv being Function of Omega,Omega2 st
     for i being Element of I holds
    rv is random_variable of El_Filtration(i,Q),Sigma2
proof
  let Omega, Omega2 be non empty set;
  let Sigma be SigmaField of Omega;
  let Sigma2 be SigmaField of Omega2;
  let I be non empty real-membered set;
  let Q be ManySortedSigmaField of I,Sigma;
   consider w being object such that A00: w in Omega2 by XBOOLE_0:def 1;
   reconsider w as Element of Omega2 by A00;
   set myset=w;
   deffunc U(Element of Omega)=myset;
   consider myfunc being Function of Omega, Omega2 such that
    B3: myfunc=Omega-->myset;
    take myfunc;
    let i be Element of I;
    myfunc is (El_Filtration(i,Q),Sigma2)-random_variable-like
    proof
     for x being set st x in Sigma2 holds myfunc"x in El_Filtration(i,Q)
     proof
      let x be set;
      assume x in Sigma2;
      per cases;
      suppose CAS0: myset in x;
       H1: myfunc"x=Omega
       proof
        for y being object holds y in myfunc"x iff y in Omega
        proof
         let y be object;
         y in Omega implies y in myfunc"x
         proof
          assume I0: y in Omega; then
          I1: y in dom myfunc by FUNCT_2:def 1;
          myfunc.y in x by I0,B3,FUNCOP_1:7,CAS0;
          hence thesis by I1,FUNCT_1:def 7;
         end;
        hence thesis;
        end;
       hence thesis by TARSKI:def 3;
       end;
      myfunc"x in Q.i
      proof
       Q.i is SigmaField of Omega by KOLMOG01:def 2;
       hence thesis by H1,PROB_1:5;
       end;
      hence thesis;
      end;
      suppose CAS1: not myset in x;
       myfunc"x c= {}
       proof
        let z be object;
         assume z in myfunc"x; then
         z in dom myfunc & myfunc.z in x & myfunc.z=myset
          by FUNCT_1:def 7, B3,FUNCOP_1:7;
         hence thesis by CAS1;
       end; then
      myfunc"x={};
      hence thesis by PROB_1:4;
      end;
     end;
    hence thesis;
    end;
   hence thesis;
 end;

:: Stochastic Process: adapted and predictable

:: The next statement is important for the usage of a probability measure
:: with Events depending on SigmaFields in a given filtration.

theorem
  for Omega being non empty set,
      Sigma being SigmaField of Omega,
      Sigma2 being SigmaField of Omega st Sigma2 c= Sigma holds
      for E2 being Event of Sigma2 holds E2 is Event of Sigma;

:: Next we define the stochastic process

definition
  let Omega,Omega2 be non empty set,
      Sigma be SigmaField of Omega,
      Sigma2 be SigmaField of Omega2,
      I be non empty real-membered set;
  mode Stochastic_Process of I,Sigma,Sigma2 ->
   Function of I,set_of_random_variables_on(Sigma,Sigma2) means :Def30000:
   for k being Element of I holds
    ex RV being Function of Omega,Omega2 st
      it.k=RV & RV is (Sigma,Sigma2)-random_variable-like;
 existence
 proof
  set q = the Element of Omega2;
  set F=Omega-->q;
  A1: F is (Sigma,Sigma2)-random_variable-like by 1A5;
   F in set_of_random_variables_on(Sigma,Sigma2) by A1; then
  reconsider F as Element of set_of_random_variables_on(Sigma,Sigma2);
  deffunc U(Element of I)=F;
  consider fI1 being
   Function of I,set_of_random_variables_on(Sigma,Sigma2) such that
   B1: for d be Element of I holds fI1.d = U(d) from FUNCT_2:sch 4;
  for k being Element of I holds
   ex RV being Function of Omega,Omega2 st
     fI1.k=RV & RV is (Sigma,Sigma2)-random_variable-like by A1,B1;
 hence thesis;
 end;
 end;

:: Because adapted and predicted stochastic processes are very important for
:: Stochastic finance, we implement them now:

definition
  let Omega,Omega2 be non empty set,
      Sigma be SigmaField of Omega,
      Sigma2 be SigmaField of Omega2,
      I be non empty real-membered set,
      Stoch be Stochastic_Process of I,Sigma,Sigma2,
      k be Element of I;
  func RVProcess(Stoch,k) -> random_variable of Sigma,Sigma2 equals
   Stoch.k;
  coherence
  proof
   consider RV being Function of Omega,Omega2 such that
    A0: Stoch.k=RV & RV is (Sigma,Sigma2)-random_variable-like by Def30000;
  thus thesis by A0;
  end;
end;

definition
  let Omega,Omega2 be non empty set,
      Sigma be SigmaField of Omega,
      Sigma2 be SigmaField of Omega2,
      I be non empty real-membered set,
      Stoch be Stochastic_Process of I,Sigma,Sigma2;
  mode Adapted_Stochastic_Process of Stoch ->
   Function of I,set_of_random_variables_on(Sigma,Sigma2) means :Def30002:
  ex k being Filtration of I,Sigma st
   for i being Element of I holds
    RVProcess(Stoch,i) is (El_Filtration(i,k),Sigma2)-random_variable-like;
 existence
 proof
  set MyBool=bool Sigma;
  D0: {Sigma} c= bool Sigma by ZFMISC_1:68;
  Sigma in {Sigma} by TARSKI:def 1; then
  reconsider Sigma as Element of MyBool by D0;
  set F=I-->Sigma;
  reconsider Sigma as SigmaField of Omega;
  W2: for i being Element of I holds F.i=Sigma by FUNCOP_1:7;
  for i being set st i in I holds F.i is SigmaField of Omega by FUNCOP_1:7;
  then reconsider F as ManySortedSigmaField of I,Sigma by KOLMOG01:def 2;
   WW1: for s,t being Element of I st s<=t holds F.s is Subset of F.t
   proof
    let s,t be Element of I;
    assume s<=t;
    F.s=Sigma by FUNCOP_1:7;
    hence thesis by FUNCOP_1:7;
   end;
  F is Filtration of I,Sigma by WW1,Def2000;
  then consider F being Filtration of I,Sigma such that
   C0: for i being Element of I holds F.i=Sigma by W2;
  for i being Element of I holds
   RVProcess(Stoch,i) is (El_Filtration(i,F),Sigma2)-random_variable-like
  proof
   let i be Element of I;
   El_Filtration(i,F) = Sigma by C0;
   hence thesis;
  end;
 hence thesis;
 end;
end;

definition
  let Omega,Omega2 be non empty set;
  let Sigma be SigmaField of Omega;
  let Sigma2 be SigmaField of Omega2;
  let I, J be non empty Subset of NAT;
  let Stoch be Stochastic_Process of In(J,bool REAL),Sigma,Sigma2;
  mode Predictable_Stochastic_Process of I,J,Sigma,Sigma2,Stoch ->
  Function of J,set_of_random_variables_on(Sigma,Sigma2) means
  ex k being Filtration of In(I,bool REAL), Sigma st
   for j being Element of In(J,bool REAL),
       i being Element of In(I,bool REAL) st j-1=i holds
    RVProcess(Stoch,j) is (El_Filtration(i,k),Sigma2)-random_variable-like;
 existence
 proof
  set MyBool=bool Sigma;
  D0: {Sigma} c= bool Sigma by ZFMISC_1:68;
  Sigma in {Sigma} by TARSKI:def 1; then
  reconsider Sigma as Element of MyBool by D0;
  set F=In(I,bool REAL)-->Sigma;
  reconsider Sigma as SigmaField of Omega;
  W2: for i being Element of In(I,bool REAL) holds F.i=Sigma by FUNCOP_1:7;
  for i being set st i in In(I,bool REAL) holds
   F.i is SigmaField of Omega by FUNCOP_1:7; then
  reconsider F as ManySortedSigmaField of In(I,bool REAL),Sigma
   by KOLMOG01:def 2;
   for s,t being Element of In(I,bool REAL)
        st s<=t holds F.s is Subset of F.t
   proof
    let s,t be Element of In(I,bool REAL);
    assume s<=t;
    F.s=Sigma by FUNCOP_1:7;
   hence thesis by FUNCOP_1:7;
   end; then
  F is Filtration of In(I,bool REAL),Sigma by Def2000; then
  consider F being Filtration of In(I,bool REAL),Sigma such that
   C0: for i being Element of In(I,bool REAL) holds F.i=Sigma by W2;
  for j being Element of In(J,bool REAL),
      i being Element of In(I,bool REAL)st j-1=i holds
    RVProcess(Stoch,j) is (El_Filtration(i,F),Sigma2)-random_variable-like
  proof
   let j be Element of In(J,bool REAL);
   let i be Element of In(I,bool REAL);
   assume j-1=i;
   Sigma = El_Filtration(i,F) by C0;
   hence thesis;
  end;
 hence thesis;
 end;
end;

definition
  let Omega,Omega2 be non empty set;
  let Sigma be SigmaField of Omega;
  let Sigma2 be SigmaField of Omega2;
  let I be non empty real-membered set;
  let MyFunc be ManySortedSigmaField of I,Sigma;
  let Stoch be Stochastic_Process of I,Sigma,Sigma2;
  attr Stoch is (MyFunc)-stoch_proc_wrt_to_Filtration means
   for i being Element of I holds
   RVProcess(Stoch,i) is
     (El_Filtration(i,MyFunc),Sigma2)-random_variable-like;
end;

theorem
  for Omega,Omega2 being non empty set,
      Sigma being SigmaField of Omega,
      Sigma2 being SigmaField of Omega2,
      I being non empty real-membered set,
      MyFunc being Filtration of I,Sigma,
      Stoch being Stochastic_Process of I,Sigma,Sigma2 st
    Stoch is (MyFunc)-stoch_proc_wrt_to_Filtration holds
    Stoch is Adapted_Stochastic_Process of Stoch by Def30002;

:: Example for a Stochastic Process

definition
  let k1,k2 be Element of REAL;
  let Omega be non empty set;
  let k be Element of Omega;
  func Set1_for_RandomVariable(k1,k2,k) -> Element of REAL equals
    k1 if (k=1 or k=2) otherwise k2;
  correctness;
  func Set4_for_RandomVariable(k1,k2,k) -> Element of REAL equals :Def79:
    k1 if k=3 otherwise k2;
  correctness;
end;

definition
  let k2,k3,k4 be Element of REAL;
  let Omega be non empty set;
  let k be Element of Omega;
  func Set3_for_RandomVariable(k2,k3,k4,k) -> Element of REAL equals :Def78:
  k2 if k=2 otherwise Set4_for_RandomVariable(k3,k4,k);
  correctness;
end;

definition
  let k1,k2,k3,k4 be Element of REAL;
  let Omega be non empty set;
  let k be Element of Omega;
  func Set2_for_RandomVariable(k1,k2,k3,k4,k) -> Element of REAL equals:Def77:
   k1 if k=1 otherwise Set3_for_RandomVariable(k2,k3,k4,k);
  correctness;
end;

theorem MYF30:
  for k1,k2,k3,k4 being Element of REAL holds
  for Omega being set st Omega={1,2,3,4}
  ex f being Function of Omega,REAL st
   f.1=k1 & f.2=k2 & f.3=k3 & f.4=k4
 proof
  let k1,k2,k3,k4 be Element of REAL;
  let Omega be set;
  assume ASS: Omega={1,2,3,4};
A1: 1 in Omega by ENUMSET1:def 2,ASS;
A2: 2 in Omega by ENUMSET1:def 2,ASS;
A3: 3 in Omega by ENUMSET1:def 2,ASS;
A4: 4 in Omega by ENUMSET1:def 2,ASS;
  reconsider Omega as non empty set by ASS;
   deffunc U(Element of Omega)=Set2_for_RandomVariable(k1,k2,k3,k4,$1);
       consider f being Function of Omega,REAL such that
   B1: for d being Element of Omega holds f.d = U(d) from FUNCT_2:sch 4;
   B2: f.1=k1
   proof
    consider k being Element of Omega such that C1: k=1 by A1;
    f.k=Set2_for_RandomVariable(k1,k2,k3,k4,k) by B1;
    hence thesis by C1, Def77;
   end;
   B3: f.2=k2
   proof
    consider k being Element of Omega such that C1: k=2 by A2;
    f.2=Set2_for_RandomVariable(k1,k2,k3,k4,k) & k=2 by B1, C1;
    then f.2=Set3_for_RandomVariable(k2,k3,k4,k) & k=2 by Def77;
    hence thesis by Def78;
   end;
   B4: f.3=k3
   proof
    consider k being Element of Omega such that C1: k=3 by A3;
    f.k=Set2_for_RandomVariable(k1,k2,k3,k4,k) by B1;
    then f.3=Set3_for_RandomVariable(k2,k3,k4,k) & k=3 by C1,Def77;
    then f.3=Set4_for_RandomVariable(k3,k4,k) & k=3 by Def78;
    hence thesis by Def79;
   end;
   f.4=k4
   proof
    consider k being Element of Omega such that C1: k=4 by A4;
    f.k=Set2_for_RandomVariable(k1,k2,k3,k4,k) by B1;
    then f.4=Set3_for_RandomVariable(k2,k3,k4,k) & k=4 by C1, Def77;
    then f.4=Set4_for_RandomVariable(k3,k4,k) & k=4 by Def78;
    hence thesis by Def79;
   end;
   hence thesis by B2,B3,B4;
 end;

theorem MyFunc5:
  for k1,k2,k3,k4 be Element of REAL holds
  for Omega being non empty set st Omega={1,2,3,4} holds
  for Sigma being SigmaField of Omega,
      I being non empty real-membered set,
      MyFunc being ManySortedSigmaField of I,Sigma st
      MyFunc.1=Special_SigmaField1 &
      MyFunc.2=Special_SigmaField2 &
      MyFunc.3=Trivial-SigmaField {1,2,3,4} holds
        for eli being Element of I st eli=3 holds
    ex f being Function of Omega,REAL st
     f.1=k1 & f.2=k2 & f.3=k3 & f.4=k4 &
     f is (El_Filtration(eli,MyFunc),Borel_Sets)-random_variable-like
 proof
  let k1,k2,k3,k4 be Element of REAL;
  let Omega be non empty set;
  assume A0: Omega={1,2,3,4};
  let Sigma be SigmaField of Omega;
  let I be non empty real-membered set;
  let MyFunc be ManySortedSigmaField of I,Sigma;
  assume A2: MyFunc.1=Special_SigmaField1 & MyFunc.2=Special_SigmaField2 &
             MyFunc.3=Trivial-SigmaField {1,2,3,4};
  let eli be Element of I;
  assume A4: eli=3;
   consider f being Function of Omega,REAL such that
   A3: f.1=k1 & f.2=k2 & f.3=k3 & f.4=k4 by A0,MYF30;
   II0: for x being object holds
         x in dom f implies (x=1 or x=2 or x=3 or x=4) by A0,ENUMSET1:def 2;
   II: 1 in dom f & 2 in dom f & 3 in dom f & 4 in dom f
   proof
     dom f = {1,2,3,4} by FUNCT_2:def 1,A0;
     hence thesis by ENUMSET1:def 2;
   end;
   f is (El_Filtration(eli,MyFunc),Borel_Sets)-random_variable-like
   proof
   set i=eli;
    for x being set holds f"x in El_Filtration(i,MyFunc)
    proof
     let x be set;
      f"x in MyFunc.i
      proof
       f"x in bool {1,2,3,4}
       proof
        per cases;
        suppose ASUPP1: k1 in x;
         per cases;
         suppose BSUPP1: k2 in x;
          per cases;
          suppose CSUPP1: k3 in x;
           per cases;
           suppose DSUPP1: k4 in x;
            for z being object holds
              z in {1,2,3,4} iff ex y being object st [z,y] in f & y in x
            proof
             let z be object;
             thus z in {1,2,3,4} implies
                ex y being object st [z,y] in f & y in x
             proof
              assume z in {1,2,3,4}; then
              z in dom f by FUNCT_2:def 1, A0; then
              consider y being object such that K01: y=f.z & z in dom f;
              Fin1: [z,y] in f by K01,FUNCT_1:1;
              y in x by K01,A0,ENUMSET1:def 2,A3,ASUPP1,BSUPP1,CSUPP1,DSUPP1;
              hence thesis by Fin1;
             end;
             given y being object such that U000:[z,y] in f & y in x;
             z=1 or z=2 or z=3 or z=4 by U000,FUNCT_1:1,II0;
             hence thesis by ENUMSET1:def 2;
            end; then
           f"x={1,2,3,4} by RELAT_1:def 14;
           hence thesis;
           end;
           suppose DSUPP2: not k4 in x;
            for z being object holds
              z in {1,2,3} iff ex y being object st [z,y] in f & y in x
            proof
             let z be object;
             thus z in {1,2,3} implies
                   ex y being object st [z,y] in f & y in x
             proof
              assume z in {1,2,3}; then
        SS:   z = 1 or z = 2 or z = 3 by ENUMSET1:def 1; then
              consider y being object such that K01: y=f.z & z in dom f
                by II;
              [z,y] in f by K01,FUNCT_1:1;
              hence thesis by A3,ASUPP1,K01,BSUPP1,CSUPP1,SS;
             end;
             given y being object such that U000:[z,y] in f & y in x;
             z <> 4 by A3, U000,FUNCT_1:1, DSUPP2; then
             z=1 or z=2 or z=3 by U000,FUNCT_1:1, II0;
             hence thesis by ENUMSET1:def 1;
            end;
           hence thesis by B123,RELAT_1:def 14;
           end;
          end;
          suppose CSUPP2: not k3 in x;
           per cases;
           suppose DSUPP1: k4 in x;
            for z being object holds
              z in {1,2,4} iff ex y being object st [z,y] in f & y in x
            proof
             let z be object;
             thus z in {1,2,4} implies
               ex y being object st [z,y] in f & y in x
             proof
              assume z in {1,2,4}; then
SS:           z = 1 or z = 2 or z = 4 by ENUMSET1:def 1; then
              consider y being object such that K01: y=f.z & z in dom f by II;
              [z,y] in f by K01,FUNCT_1:1;
              hence thesis by SS,A3,ASUPP1, K01,BSUPP1,DSUPP1;
             end;
             given y being object such that U000:[z,y] in f & y in x;
             z <> 3 by A3,U000,FUNCT_1:1,CSUPP2; then
             z=1 or z=2 or z=4 by II0,U000,FUNCT_1:1;
             hence thesis by ENUMSET1:def 1;
            end;
           hence thesis by B124,RELAT_1:def 14;
           end;
           suppose DSUPP2: not k4 in x;
           Fin1: for z being object holds z in {1,2} iff
               ex y being object st [z,y] in f & y in x
            proof
             let z be object;
             thus z in {1,2} implies
               ex y being object st [z,y] in f & y in x
             proof
              assume z in {1,2}; then
SS:           z = 1 or z = 2 by TARSKI:def 2; then
              consider y being object such that K01: y=f.z & z in dom f by II;
              [z,y] in f by K01,FUNCT_1:1;
              hence thesis by A3, ASUPP1,K01,BSUPP1,SS;
             end;
             given y being object such that U000:[z,y] in f & y in x;
             z <> 3 & z <> 4 by A3,U000,FUNCT_1:1,CSUPP2,DSUPP2; then
             z=1 or z=2 by U000,FUNCT_1:1,II0;
             hence thesis by TARSKI:def 2;
            end;
           {1,2} in bool {1,2,3,4} by Lm2;
           hence thesis by Fin1,RELAT_1:def 14;
           end;
          end;
         end;
         suppose BSUPP1: not k2 in x;
          per cases;
          suppose CSUPP1: k3 in x;
           per cases;
           suppose DSUPP1: k4 in x;
            for z being object holds
              z in {1,3,4} iff ex y being object st [z,y] in f & y in x
            proof
             let z be object;
             thus z in {1,3,4} implies
                   ex y being object st [z,y] in f & y in x
             proof
              assume z in {1,3,4}; then
SS:           z = 1 or z = 3 or z = 4 by ENUMSET1:def 1; then
              consider y being object such that K01: y=f.z & z in dom f by II;
              [z,y] in f by K01,FUNCT_1:1;
              hence thesis by A3,ASUPP1,K01,SS,CSUPP1,DSUPP1;
             end;
             given y being object such that U000:[z,y] in f & y in x;
             z <> 2 by A3,U000,FUNCT_1:1,BSUPP1; then
             z=1 or z=3 or z=4 by U000,FUNCT_1:1,II0;
             hence thesis by ENUMSET1:def 1;
            end;
           hence thesis by B134,RELAT_1:def 14;
           end;
           suppose DSUPP2: not k4 in x;
            for z being object holds
             z in {1,3} iff ex y being object st [z,y] in f & y in x
            proof
             let z be object;
             thus z in {1,3} implies
                   ex y being object st [z,y] in f & y in x
             proof
              assume z in {1,3}; then
SS:           z = 1 or z = 3 by TARSKI:def 2; then
              consider y being object such that K01: y=f.z & z in dom f by II;
              [z,y] in f by K01,FUNCT_1:1;
              hence thesis by A3, ASUPP1,K01,CSUPP1,SS;
             end;
              given y being object such that U000:[z,y] in f & y in x;
              z <> 2 & z <> 4 by A3, U000,FUNCT_1:1,BSUPP1,DSUPP2; then
              z=1 or z=3 by U000,FUNCT_1:1, II0;
             hence thesis by TARSKI:def 2;
            end;
           hence thesis by B13,RELAT_1:def 14;
           end;
          end;
          suppose CSUPP2: not k3 in x;
           per cases;
           suppose DSUPP1: k4 in x;
            for z being object holds
              z in {1,4} iff ex y being object st [z,y] in f & y in x
            proof
             let z be object;
             thus z in {1,4} implies
                   ex y being object st [z,y] in f & y in x
             proof
              assume z in {1,4}; then
SS:           z = 1 or z = 4 by TARSKI:def 2; then
              consider y being object such that K01: y=f.z & z in dom f by II;
              [z,y] in f by K01,FUNCT_1:1;
              hence thesis by A3, ASUPP1,K01,SS,DSUPP1;
             end;
             given y being object such that U000:[z,y] in f & y in x;
             z <> 2 & z <> 3 by A3, U000,FUNCT_1:1,BSUPP1,CSUPP2; then
             z=1 or z=4 by U000,FUNCT_1:1, II0;
             hence thesis by TARSKI:def 2;
            end;
           hence thesis by B14,RELAT_1:def 14;
           end;
           suppose DSUPP2: not k4 in x;
            Fin1: for z being object holds
              z in {1} iff ex y being object st [z,y] in f & y in x
            proof
             let z be object;
             thus z in {1} implies
                   ex y being object st [z,y] in f & y in x
             proof
              assume K000: z in {1}; then
              z in dom f by TARSKI:def 1, II; then
              consider y being object such that K01: y=f.z & z in dom f;
              Fin1: [z,y] in f by K01,FUNCT_1:1;
              z=1 by K000,TARSKI:def 1;
              hence thesis by A3, ASUPP1, Fin1, K01;
             end;
             given y being object such that U000:[z,y] in f & y in x;
             z <> 2 & z <> 3 & z <> 4 by A3, FUNCT_1:1, U000, DSUPP2,BSUPP1,
             CSUPP2; then
             z=1 by U000,FUNCT_1:1,II0;
             hence thesis by TARSKI:def 1;
            end;
           {1} in bool {1,2,3,4} by EnLm1;
           hence thesis by Fin1,RELAT_1:def 14;
           end;
          end;
         end;
        end;
        suppose ASUPP2: not k1 in x;
         per cases;
         suppose BSUPP1: k2 in x;
          per cases;
          suppose CSUPP1: k3 in x;
           per cases;
           suppose DSUPP1: k4 in x;
            for z being object holds z in {2,3,4} iff
               ex y being object st [z,y] in f & y in x
            proof
             let z be object;
             thus z in {2,3,4} implies
                   ex y being object st [z,y] in f & y in x
             proof
              assume z in {2,3,4}; then
SS:           z = 2 or z = 3 or z = 4 by ENUMSET1:def 1; then
              consider y being object such that K01: y=f.z & z in dom f by II;
              [z,y] in f by K01,FUNCT_1:1;
              hence thesis by A3, BSUPP1, K01,SS,CSUPP1,DSUPP1;
             end;
             given y being object such that U000:[z,y] in f & y in x;
             z <> 1 by A3, FUNCT_1:1,U000, ASUPP2; then
             z=2 or z=3 or z=4 by U000,FUNCT_1:1, II0;
             hence thesis by ENUMSET1:def 1;
            end;
           hence thesis by B234,RELAT_1:def 14;
           end;
           suppose DSUPP2: not k4 in x;
            for z being object holds
              z in {2,3} iff ex y being object st [z,y] in f & y in x
            proof
             let z be object;
             thus z in {2,3} implies
                   ex y being object st [z,y] in f & y in x
             proof
              assume z in {2,3}; then
SS:           z = 2 or z = 3 by TARSKI:def 2; then
              consider y being object such that K01: y=f.z & z in dom f by II;
              [z,y] in f by K01,FUNCT_1:1;
              hence thesis by A3, BSUPP1,K01,CSUPP1,SS;
             end;
             given y being object such that U000:[z,y] in f & y in x;
             z <> 1 & z <> 4 by A3, U000,FUNCT_1:1, ASUPP2,DSUPP2; then
             z=2 or z=3 by U000,FUNCT_1:1,II0;
             hence thesis by TARSKI:def 2;
            end;
           hence thesis by B23,RELAT_1:def 14;
           end;
          end;
          suppose CSUPP1: not k3 in x;
           per cases;
           suppose DSUPP1: k4 in x;
            for z being object holds z in {2,4} iff
               ex y being object st [z,y] in f & y in x
            proof
             let z be object;
             thus z in {2,4} implies
                   ex y being object st [z,y] in f & y in x
             proof
              assume z in {2,4}; then
           SS:z = 2 or z = 4 by TARSKI:def 2; then
              consider y being object such that K01: y=f.z & z in dom f by II;
              [z,y] in f by K01,FUNCT_1:1;
              hence thesis by A3, BSUPP1,K01,DSUPP1,SS;
             end;
             given y being object such that U000:[z,y] in f & y in x;
             z <> 3 & z <> 1 by A3,U000,FUNCT_1:1,ASUPP2,CSUPP1; then
             z=2 or z=4 by U000,FUNCT_1:1,II0;
             hence thesis by TARSKI:def 2;
            end;
           hence thesis by B24,RELAT_1:def 14;
           end;
           suppose DSUPP2: not k4 in x;
           Fin1: for z being object holds
              z in {2} iff ex y being object st [z,y] in f & y in x
            proof
             let z be object;
             thus z in {2} implies
                   ex y being object st [z,y] in f & y in x
             proof
              assume K000: z in {2}; then
              z in dom f by TARSKI:def 1, II; then
              consider y being object such that K01: y=f.z & z in dom f;
              Fin1: [z,y] in f by K01,FUNCT_1:1;
              z=2 by K000, TARSKI:def 1;
              hence thesis by A3, BSUPP1, Fin1,K01;
             end;
             given y being object such that U000:[z,y] in f & y in x;
             z <> 1 & z <> 3 & z <> 4 by A3,U000,FUNCT_1:1,ASUPP2,DSUPP2,
                CSUPP1; then
             z=2 by U000,FUNCT_1:1,II0;
             hence thesis by TARSKI:def 1;
            end;
           {2} in bool {1,2,3,4} by EnLm2;
           hence thesis by Fin1,RELAT_1:def 14;
           end;
          end;
         end;
         suppose BSUPP2: not k2 in x;
          per cases;
          suppose CSUPP1: k3 in x;
           per cases;
           suppose DSUPP1: k4 in x;
            Fin1: for z being object holds
              z in {3,4} iff ex y being object st [z,y] in f & y in x
            proof
             let z be object;
             thus z in {3,4} implies
                   ex y being object st [z,y] in f & y in x
             proof
              assume z in {3,4}; then
SS:           z = 3 or z = 4 by TARSKI:def 2; then
              consider y being object such that K01: y=f.z & z in dom f by II;
              [z,y] in f by K01,FUNCT_1:1;
              hence thesis by A3, CSUPP1,K01,DSUPP1,SS;
             end;
             given y being object such that U000:[z,y] in f & y in x;
             z <> 1 & z <> 2 by A3, U000,FUNCT_1:1, BSUPP2,ASUPP2; then
             z=3 or z=4 by U000,FUNCT_1:1, II0;
             hence thesis by TARSKI:def 2;
            end;
           {3,4} in bool {1,2,3,4} by Lm1;
           hence thesis by Fin1,RELAT_1:def 14;
           end;
           suppose DSUPP2: not k4 in x;
            Fin1: for z being object holds
              z in {3} iff ex y being object st [z,y] in f & y in x
            proof
             let z be object;
             thus z in {3} implies
                   ex y being object st [z,y] in f & y in x
             proof
              assume K000: z in {3}; then
              z in dom f by TARSKI:def 1, II; then
              consider y being object such that K01: y=f.z & z in dom f;
              Fin1: [z,y] in f by K01,FUNCT_1:1;
              z = 3 by K000,TARSKI:def 1;
              hence thesis by A3,CSUPP1,Fin1,K01;
             end;
              given y being object such that U000:[z,y] in f & y in x;
              z <> 1 & z <> 2 & z <> 4 by A3,U000,FUNCT_1:1,BSUPP2,DSUPP2,
                ASUPP2; then
              z=3 by U000,FUNCT_1:1,II0;
              hence thesis by TARSKI:def 1;
            end;
           {3} in bool {1,2,3,4} by EnLm3;
           hence thesis by Fin1,RELAT_1:def 14;
           end;
          end;
          suppose CSUPP2: not k3 in x;
           per cases;
           suppose DSUPP1: k4 in x;
            Fin1: for z being object holds
              z in {4} iff ex y being object st [z,y] in f & y in x
            proof
             let z be object;
             thus z in {4} implies
                   ex y being object st [z,y] in f & y in x
             proof
              assume K000: z in {4}; then
              z in dom f by TARSKI:def 1, II; then
              consider y being object such that K01: y=f.z & z in dom f;
              Fin1: [z,y] in f by K01,FUNCT_1:1;
              z=4 by K000,TARSKI:def 1;
              hence thesis by A3, DSUPP1, Fin1,K01;
             end;
             given y being object such that U000:[z,y] in f & y in x;
             z <> 1 & z <> 2 & z <> 3 by A3, U000,FUNCT_1:1, CSUPP2,
             ASUPP2,BSUPP2; then
             z=4 by II0,U000,FUNCT_1:1;
             hence thesis by TARSKI:def 1;
            end;
           {4} in bool {1,2,3,4} by EnLm4;
           hence thesis by Fin1,RELAT_1:def 14;
           end;
           suppose DSUPP2: not k4 in x;
             for z being object holds
              z in {} iff ex y being object st [z,y] in f & y in x
             proof
              let z be object;
              (ex y being object st [z,y] in f & y in x) implies z in {}
              proof
               given y being object such that W1: [z,y] in f & y in x;
               z in dom f & y = f.z by W1, FUNCT_1:1;
               hence thesis by A3,W1,ASUPP2,BSUPP2,CSUPP2,
                DSUPP2,A0,ENUMSET1:def 2;
              end;
             hence thesis;
             end;
             then f"x={} by RELAT_1:def 14;
            hence thesis by PROB_1:4;
           end;
          end;
         end;
        end;
       end;
      hence thesis by A4,A2;
      end;
    hence thesis;
    end;
   hence thesis;
   end;
  hence thesis by A3;
 end;

theorem MyFunc6:
  for k1,k2 being Element of REAL,
      Omega being non empty set st Omega={1,2,3,4} holds
  for Sigma being SigmaField of Omega,
      I being non empty real-membered set,
      MyFunc being ManySortedSigmaField of I,Sigma st
      MyFunc.1=Special_SigmaField1 &
      MyFunc.2=Special_SigmaField2 &
      MyFunc.3=Trivial-SigmaField {1,2,3,4} holds
        for eli being Element of I st eli=2 holds
    ex f being Function of Omega,REAL st
     f.1=k1 & f.2=k1 & f.3=k2 & f.4=k2 &
     f is (El_Filtration(eli,MyFunc),Borel_Sets)-random_variable-like
 proof
   let k1,k2 be Element of REAL;
   let Omega be non empty set;
   assume A0: Omega={1,2,3,4};
   let Sigma be SigmaField of Omega;
   let I be non empty real-membered set;
   let MyFunc be ManySortedSigmaField of I,Sigma;
   assume A2: MyFunc.1=Special_SigmaField1 & MyFunc.2=Special_SigmaField2 &
              MyFunc.3=Trivial-SigmaField {1,2,3,4};
   let eli be Element of I;
   assume A4: eli=2;
   consider f being Function of Omega,REAL such that
   A3: f.1=k1 & f.2=k1 & f.3=k2 & f.4=k2 by A0,MYF30;
   take f;
  set i=eli;
    for x being set holds f"x in El_Filtration(i,MyFunc)
    proof
     let x be set;
      f"x in MyFunc.i
      proof
       f"x in {{},{1,2},{3,4},{1,2,3,4}}
       proof
         f"x={} or f"x={1,2} or f"x={3,4} or f"x={1,2,3,4}
         proof
         per cases;
         suppose INITSUPP: k1 in x;
          per cases;
          suppose JSUPP1: k2 in x;
            for z being object holds z in {1,2,3,4} iff
              ex y being object st [z,y] in f & y in x
            proof
             let z be object;
             I1: z in {1,2,3,4} implies
                  ex y being object st [z,y] in f & y in x
             proof
              assume ASSJ0: z in {1,2,3,4}; then
              L1: z in dom f by FUNCT_2:def 1,A0;
               per cases by ASSJ0,ENUMSET1:def 2;
               suppose z=1 or z = 2; then
               [z,k1] in f & k1 in x by A3,INITSUPP,L1,FUNCT_1:1;
               hence thesis;
               end;
               suppose z=3 or z = 4; then
               f.z=k2 & k2 in x & z in dom f
                by A3,JSUPP1,ASSJ0,FUNCT_2:def 1,A0; then
               [z,k2] in f & k2 in x by FUNCT_1:1;
               hence thesis;
               end;
             end;
             (ex y being object st [z,y] in f & y in x) implies
              z in {1,2,3,4}
             proof
              given y being object such that ASSJ0: [z,y] in f & y in x;
              z in dom f & y=f.z by ASSJ0, FUNCT_1:1;
              hence thesis by A0;
             end;
            hence thesis by I1;
            end;
           hence thesis by RELAT_1:def 14;
          end;
          suppose JSUPP2: not k2 in x;
           for z being object holds
            z in {1,2} iff ex y being object st [z,y] in f & y in x
           proof
            let z be object;
            I1: z in {1,2} implies
                  ex y being object st [z,y] in f & y in x
            proof
             assume z in {1,2}; then
S2:          z = 1 or z = 2 by TARSKI:def 2; then
             z in Omega by ENUMSET1:def 2,A0; then
S1:          z in dom f by FUNCT_2:def 1;
             [z,k1] in f by S1,S2,A3,FUNCT_1:1;
             hence thesis by INITSUPP;
            end;
            (ex y being object st [z,y] in f & y in x) implies z in {1,2}
            proof
             given y being object such that
             M1: [z,y] in f & y in x;
             z in dom f by M1,FUNCT_1:1; then
             z=1 or z=2 or z=3 or z=4 by A0,ENUMSET1:def 2;
             hence thesis by JSUPP2,M1,FUNCT_1:1,A3,TARSKI:def 2;
             end;
            hence thesis by I1;
            end;
           hence thesis by RELAT_1:def 14;
           end;
          end;
         suppose INITSUPP: not k1 in x;
          per cases;
          suppose JSUPP1: k2 in x;
            for z being object holds z in {3,4} iff
              ex y being object st [z,y] in f & y in x
            proof
             let z be object;
             I1: z in {3,4} implies ex y being object st [z,y] in f & y in x
             proof
              assume z in {3,4}; then
              J1: z = 3 or z = 4 by TARSKI:def 2; then
              z in {1,2,3,4} by ENUMSET1:def 2; then
              z in dom f by FUNCT_2:def 1, A0; then
              [z,k2] in f by J1,A3,FUNCT_1:1;
              hence thesis by JSUPP1;
             end;
             (ex y being object st [z,y] in f & y in x) implies
              z in {3,4}
             proof
              given y being object such that ASSJ0: [z,y] in f & y in x;
                OO0: y=k1 or y=k2
                proof
                 z in dom f by ASSJ0,FUNCT_1:1; then
                 z = 1 or z = 2 or z = 3 or z = 4 by ENUMSET1:def 2,A0;
                 hence thesis by A3,ASSJ0,FUNCT_1:1;
                end;
                Z10: k2=f.z
                proof
                 per cases by OO0;
                 suppose y=k1;
                 hence thesis by INITSUPP,ASSJ0;
                 end;
                 suppose y=k2;
                 hence thesis by ASSJ0,FUNCT_1:1;
                 end;
                end;
                z=3 or z=4
                proof
                  assume ZZ1: z<>3 & z<>4;
                  z in dom f by ASSJ0,FUNCT_1:1;
                  hence thesis by Z10,ZZ1,A3,INITSUPP,
                    JSUPP1,ENUMSET1:def 2,A0;
                end;
             hence thesis by TARSKI:def 2;
             end;
            hence thesis by I1;
            end;
           hence thesis by RELAT_1:def 14;
          end;
          suppose JSUPP2: not k2 in x;
           for z being object holds
            z in {} iff ex y being object st [z,y] in f & y in x
           proof
            let z be object;
            (ex y being object st [z,y] in f & y in x) implies z in {}
            proof
             given y being object such that
              M1: [z,y] in f & y in x;
              z in dom f & y =f.z & y <> k2 by M1,FUNCT_1:1,JSUPP2;
             hence thesis by INITSUPP,M1,A3,A0,ENUMSET1:def 2;
             end;
            hence thesis;
           end;
           hence thesis by RELAT_1:def 14;
           end;
         end;
        end;
        hence thesis by ENUMSET1:def 2;
       end;
       hence thesis by A4,A2;
       end;
     hence thesis;
    end;
    hence thesis by A3;
 end;

theorem MyFunc7:
  for k1 being Element of REAL,
      Omega being non empty set st Omega={1,2,3,4} holds
  for Sigma being SigmaField of Omega,
      I being non empty real-membered set,
      MyFunc being ManySortedSigmaField of I,Sigma st
      MyFunc.1=Special_SigmaField1 &
      MyFunc.2=Special_SigmaField2 &
      MyFunc.3=Trivial-SigmaField {1,2,3,4} holds
        for eli being Element of I st eli=1 holds
    ex f being Function of Omega,REAL st
     f.1=k1 & f.2=k1 & f.3=k1 & f.4=k1 &
     f is (El_Filtration(eli,MyFunc),Borel_Sets)-random_variable-like
 proof
   let k1 be Element of REAL;
   let Omega be non empty set;
   assume A0: Omega={1,2,3,4};
   let Sigma be SigmaField of Omega;
   let I be non empty real-membered set;
   let MyFunc be ManySortedSigmaField of I,Sigma;
   assume A2: MyFunc.1=Special_SigmaField1 & MyFunc.2=Special_SigmaField2 &
              MyFunc.3=Trivial-SigmaField {1,2,3,4};
   let eli be Element of I;
   assume A4: eli=1;
    consider f being Function of Omega,REAL such that
A3: f.1=k1 & f.2=k1 & f.3=k1 & f.4=k1 by A0,MYF30;
   take f;
    set i=eli;
     for x being set holds f"x in El_Filtration(i,MyFunc)
     proof
      let x be set;
       f"x in MyFunc.i
       proof
        f"x in {{},{1,2,3,4}}
        proof
          f"x={} or f"x={1,2,3,4}
          proof
           per cases;
           suppose JSUPP1: k1 in x;
             for z being object holds z in {1,2,3,4} iff
               ex y being object st [z,y] in f & y in x
             proof
              let z be object;
          I1: z in {1,2,3,4} implies
                   ex y being object st [z,y] in f & y in x
              proof
               assume ASSJ0: z in {1,2,3,4};
               [z,k1] in f
               proof
                z in dom f & k1 = f.z by ENUMSET1:def 2,A3,
                                         ASSJ0,FUNCT_2:def 1,A0;
               hence thesis by FUNCT_1:1;
               end;
              hence thesis by JSUPP1;
              end;
              (ex y being object st [z,y] in f & y in x) implies
               z in {1,2,3,4}
              proof
               given y being object such that ASSJ0: [z,y] in f & y in x;
               z in dom f & y=f.z by ASSJ0, FUNCT_1:1;
               hence thesis by A0;
              end;
             hence thesis by I1;
             end;
            hence thesis by RELAT_1:def 14;
           end;
           suppose JSUPP2: not k1 in x;
            for z being object holds z in {} iff
              ex y being object st [z,y] in f & y in x
            proof
             let z be object;
             (ex y being object st [z,y] in f & y in x) implies z in {}
              proof
              given y being object such that
               M1: [z,y] in f & y in x;
               z in dom f & y =f.z & not y=k1 by M1,FUNCT_1:1, JSUPP2;
               hence thesis by A3,A0,ENUMSET1:def 2;
              end;
            hence thesis;
            end;
            hence thesis by RELAT_1:def 14;
            end;
          end;
         hence thesis by TARSKI:def 2;
         end;
        hence thesis by A4,A2;
        end;
     hence thesis;
     end;
  hence thesis by A3;
 end;

theorem
  for Omega being non empty set st Omega={1,2,3,4} holds
  for Sigma being SigmaField of Omega,
      I being non empty real-membered set
    st I={1,2,3} & Sigma = bool {1,2,3,4} holds
    for MyFunc being ManySortedSigmaField of I,Sigma st
      MyFunc.1=Special_SigmaField1 &
      MyFunc.2=Special_SigmaField2 &
      MyFunc.3=Trivial-SigmaField {1,2,3,4} holds
       for Prob being Function of Sigma, REAL holds
         for i being Element of I holds
          ex RV being Function of Omega,REAL st
           RV is (El_Filtration(i,MyFunc),Borel_Sets)-random_variable-like
 proof
  let Omega be non empty set;
  assume A0: Omega={1,2,3,4};
  let Sigma be SigmaField of Omega;
  let I be non empty real-membered set;
  assume A1: I={1,2,3} & Sigma=bool{1,2,3,4};
  let MyFunc be ManySortedSigmaField of I,Sigma;
  assume A2: MyFunc.1=Special_SigmaField1 & MyFunc.2=Special_SigmaField2 &
             MyFunc.3=Trivial-SigmaField {1,2,3,4};
  let Prob be Function of Sigma, REAL;
  let i be Element of I;
     per cases by A1,ENUMSET1:def 1;
     suppose a1: i=1;
     100 in REAL by NUMBERS:19; then
      ex f being Function of Omega,REAL st
      f.1=100 & f.2=100 & f.3=100 & f.4=100 &
      f is (El_Filtration(i,MyFunc),Borel_Sets)-random_variable-like
      by A0,A2,MyFunc7,a1;
     hence thesis;
     end;
     suppose a1: i=2;
     80 in REAL & 120 in REAL by NUMBERS:19; then
      ex f being Function of Omega,REAL st
       f.1=80 & f.2=80 & f.3=120 & f.4=120 &
       f is (El_Filtration(i,MyFunc),Borel_Sets)-random_variable-like
      by A0,A2,MyFunc6,a1;
     hence thesis;
     end;
     suppose a1: i=3;
     60 in REAL & 80 in REAL & 100 in REAL & 120 in REAL by NUMBERS:19; then
      ex f being Function of Omega,REAL st
      f.1=60 & f.2=80 & f.3=100 & f.4=120 &
       f is (El_Filtration(i,MyFunc),Borel_Sets)-random_variable-like
      by A0,A2,MyFunc5,a1;
     hence thesis;
     end;
 end;

definition
  let I be non empty real-membered set such that A0000: I={1,2,3};
  let i be Element of I such that MyI: i=2 or i=3;
  let Omega be non empty set such that A000: Omega={1,2,3,4};
  let Sigma be SigmaField of Omega such that A00: Sigma=bool Omega;
  let f1 be Function of Omega,REAL such that
  A0: f1.1=60 & f1.2=80 & f1.3=100 & f1.4=120;
  let f2 be Function of Omega,REAL such that
  A1: f2.1=80 & f2.2=80 & f2.3=120 & f2.4=120;
  let f3 be Function of Omega,REAL;
  func FunctionRV1(i,Sigma,f1,f2,f3) -> Element of
    set_of_random_variables_on(Sigma,Borel_Sets) equals :Def1211:
     f2 if i=2 otherwise f1;
 correctness
 proof
   consider MyFunc being Filtration of I,Sigma such that
   B1: MyFunc.1=Special_SigmaField1 & MyFunc.2=Special_SigmaField2 &
        MyFunc.3=Trivial-SigmaField {1,2,3,4} by A0000,A00,A000,MyNeed;
  per cases;
  suppose SUPP: i=2;
   80 in REAL & 120 in REAL by NUMBERS:19; then
   consider f being Function of Omega,REAL such that
B4: f.1=80 & f.2=80 & f.3=120 & f.4=120 &
    f is (El_Filtration(i,MyFunc),Borel_Sets)-random_variable-like
      by A000,B1,MyFunc6,SUPP;
   f is (Sigma,Borel_Sets)-random_variable-like by A00; then
   ZW1: f in set_of_random_variables_on(Sigma,Borel_Sets);
   dom f=Omega by FUNCT_2:def 1; then
KK: dom f = dom f2 by FUNCT_2:def 1;
   for x being object st x in dom f holds f.x = f2.x
   proof
     let x be object;
     assume x in dom f;
     then reconsider x as Element of Omega;
     x = 1 or x = 2 or x = 3 or x = 4 by A000,ENUMSET1:def 2;
     hence thesis by B4, A1;
   end;
   hence thesis by ZW1,SUPP,FUNCT_1:2,KK;
  end;
  suppose F1: i <> 2;
   60 in REAL & 80 in REAL & 100 in REAL & 120 in REAL by NUMBERS:19; then
   consider f being Function of Omega,REAL such that
    B4: f.1=60 & f.2=80 & f.3=100 & f.4=120 &
     f is (El_Filtration(i,MyFunc),Borel_Sets)-random_variable-like
      by A000,B1,MyFunc5,MyI,F1;
   f is (Sigma,Borel_Sets)-random_variable-like by A00; then
   ZW1: f in set_of_random_variables_on(Sigma,Borel_Sets);
   dom f=Omega by FUNCT_2:def 1; then
KK: dom f = dom f1 by FUNCT_2:def 1;
    for x being object st x in dom f holds f.x = f1.x
    proof
     let x be object;
     assume x in dom f;
     then reconsider x as Element of Omega;
     x = 1 or x = 2 or x = 3 or x = 4 by A000,ENUMSET1:def 2;
     hence thesis by B4, A0;
    end;
    hence thesis by ZW1,F1,KK,FUNCT_1:2;
    end;
   end;
 end;

definition
  let I be non empty real-membered set such that A0000: I={1,2,3};
  let i be Element of I;
  let Omega be non empty set such that A000: Omega={1,2,3,4};
  let Sigma be SigmaField of Omega such that A00: Sigma=bool Omega;
  let f1,f2 be Function of Omega,REAL;
  let f3 be Function of Omega,REAL such that
  A2: f3.1=100 & f3.2=100 & f3.3=100 & f3.4=100;
  func FunctionRV2(i,Sigma,f1,f2,f3) ->
  Element of set_of_random_variables_on(Sigma,Borel_Sets) equals :Def1212:
    FunctionRV1(i,Sigma,f1,f2,f3) if (i=2 or i=3) otherwise f3;
 correctness
 proof
  per cases;
  suppose F1: not(i=2 or i=3);
   consider MyFunc being Filtration of I,Sigma such that
   B1:  MyFunc.1=Special_SigmaField1 & MyFunc.2=Special_SigmaField2 &
        MyFunc.3=Trivial-SigmaField {1,2,3,4} by A0000, A00,A000,MyNeed;
   B3: i=1 by F1,A0000,ENUMSET1:def 1;
   100 in REAL by NUMBERS:19; then
   consider f being Function of Omega,REAL such that
   B4: f.1=100 & f.2=100 & f.3=100 & f.4=100 &
     f is (El_Filtration(i,MyFunc),Borel_Sets)-random_variable-like
      by A000,B1,B3,MyFunc7;
   f is (Sigma,Borel_Sets)-random_variable-like by A00; then
   ZW1: f in set_of_random_variables_on(Sigma,Borel_Sets);
   dom f=Omega by FUNCT_2:def 1; then
KK: dom f = dom f3 by FUNCT_2:def 1;
   for x being object st x in dom f holds f.x = f3.x
   proof
     let x be object;
     assume x in dom f;
     then reconsider x as Element of Omega;
     x=1 or x=2 or x=3 or x=4 by A000,ENUMSET1:def 2;
     hence thesis by B4, A2;
   end;
   hence thesis by KK,ZW1,FUNCT_1:2;
  end;
  suppose i=2 or i=3;
  hence thesis;
  end;
 end;
end;

theorem
  for Omega, Omega2 being non empty set st Omega={1,2,3,4} holds
  for Sigma being SigmaField of Omega,
      I being non empty real-membered set st
    I={1,2,3} & Sigma=bool{1,2,3,4} holds
    for MyFunc being Filtration of I,Sigma st
      MyFunc.1=Special_SigmaField1 &
      MyFunc.2=Special_SigmaField2 &
      MyFunc.3=Trivial-SigmaField {1,2,3,4}
    ex Stoch being Stochastic_Process of I,Sigma,Borel_Sets st
       (for k being Element of I holds
       (ex RV being Function of Omega,REAL st
       (Stoch.k=RV & RV is (Sigma,Borel_Sets)-random_variable-like) &
         RV is (El_Filtration(k,MyFunc),Borel_Sets)-random_variable-like) &
         (ex f being Function of Omega,REAL st
             k=1 implies f.1=100 & f.2=100 & f.3=100 & f.4=100 & Stoch.k=f)&
         (ex f being Function of Omega,REAL st
             k=2 implies f.1=80 & f.2=80 & f.3=120 & f.4=120 & Stoch.k=f) &
         (ex f being Function of Omega,REAL st
             k=3 implies f.1=60 & f.2=80 & f.3=100 & f.4=120 & Stoch.k=f) &
           Stoch is (MyFunc)-stoch_proc_wrt_to_Filtration) &
           Stoch is Adapted_Stochastic_Process of Stoch
 proof
  let Omega, Omega2 be non empty set;
  assume A00: Omega={1,2,3,4};
  let Sigma be SigmaField of Omega;
  let I be non empty real-membered set;
  assume that A0: I={1,2,3} and a0: Sigma=bool{1,2,3,4};
  let MyFunc be Filtration of I,Sigma;
  assume A1: MyFunc.1=Special_SigmaField1 &
             MyFunc.2=Special_SigmaField2 &
             MyFunc.3=Trivial-SigmaField {1,2,3,4};
a1:100 in REAL by NUMBERS:19; then
  consider f3 being Function of Omega,REAL such that
   F1: f3.1=100 & f3.2=100 & f3.3=100 & f3.4=100 by A00,MYF30;
a2:80 in REAL & 120 in REAL by NUMBERS:19; then
  consider f2 being Function of Omega,REAL such that
   F2: f2.1=80 & f2.2=80 & f2.3=120 & f2.4=120 by A00,MYF30;
  60 in REAL by NUMBERS:19; then
  consider f1 being Function of Omega,REAL such that
   F3: f1.1=60 & f1.2=80 & f1.3=100 & f1.4=120 by A00,MYF30,a1,a2;
   deffunc U(Element of I)=FunctionRV2($1,Sigma,f1,f2,f3);
   consider fI1 being
   Function of I,set_of_random_variables_on(Sigma,Borel_Sets) such that
   B1: for d be Element of I holds fI1.d = U(d) from FUNCT_2:sch 4;
  Fin1: for k being Element of I holds
   ex RV being Function of Omega,REAL st
     (fI1.k=RV & RV is (Sigma,Borel_Sets)-random_variable-like)
  proof
   let k be Element of I;
   fI1.k in set_of_random_variables_on(Sigma,Borel_Sets);
   hence thesis;
  end; then
  reconsider fI1 as Stochastic_Process of I,Sigma,Borel_Sets by Def30000;
  take fI1;
    for k being Element of I holds
           (ex RV being Function of Omega,REAL st
            (fI1.k=RV & RV is (Sigma,Borel_Sets)-random_variable-like) &
            RV is (El_Filtration(k,MyFunc),Borel_Sets)-random_variable-like)
              &
              (ex f being Function of Omega,REAL st
               k=1 implies f.1=100 & f.2=100 & f.3=100 & f.4=100 & fI1.k=f) &
              (ex f being Function of Omega,REAL st
               k=2 implies f.1=80 & f.2=80 & f.3=120 & f.4=120 & fI1.k=f) &
              (ex f being Function of Omega,REAL st
             k=3 implies f.1=60 & f.2=80 & f.3=100 & f.4=120 & fI1.k=f) &
             fI1 is (MyFunc)-stoch_proc_wrt_to_Filtration &
        fI1 is Adapted_Stochastic_Process of fI1
  proof
  let k be Element of I;
  Fin3: fI1 is (MyFunc)-stoch_proc_wrt_to_Filtration
  proof
   for i being Element of I holds
   RVProcess(fI1,i) is
     (El_Filtration(i,MyFunc),Borel_Sets)-random_variable-like
   proof
    let i be Element of I;
    per cases by A0,ENUMSET1:def 1;
   suppose SUPP: i=1; then
   X1: FunctionRV2(i,Sigma,f1,f2,f3) = f3 by a0,A0,A00,F1,Def1212;
    100 in REAL by NUMBERS:19; then
    consider f being Function of Omega,REAL such that
     Q1: f.1=100 & f.2=100 & f.3=100 & f.4=100 &
       f is (El_Filtration(i,MyFunc),Borel_Sets)-random_variable-like
        by SUPP,A00,A1,MyFunc7;
    E1: dom f=Omega by FUNCT_2:def 1;
      for x being object st x in dom f holds f.x = f3.x
      proof
       let x be object;
       assume x in dom f; then
       reconsider x as Element of Omega;
       x = 1 or x = 2 or x = 3 or x = 4 by A00,ENUMSET1:def 2;
       hence thesis by Q1,F1;
      end; then
     f3=f by E1;
     hence thesis by X1,B1,Q1;
   end;
   suppose SUPP2: i=2; then
   FunctionRV2(i,Sigma,f1,f2,f3) = FunctionRV1(i,Sigma,f1,f2,f3)
    by A0,a0,A00,F1,Def1212; then
   X1: FunctionRV2(i,Sigma,f1,f2,f3) = f2 by a0,A0,A00,F2,F3,SUPP2,Def1211;
     80 in REAL & 120 in REAL by NUMBERS:19; then
    consider f being Function of Omega,REAL such that
     Q1: f.1=80 & f.2=80 & f.3=120 & f.4=120 &
       f is (El_Filtration(i,MyFunc),Borel_Sets)-random_variable-like
        by SUPP2,A00,A1,MyFunc6;
   E1: dom f=Omega by FUNCT_2:def 1;
   for x being object st x in dom f holds f.x = f2.x
   proof
     let x be object;
     assume x in dom f; then
     reconsider x as Element of Omega;
     x = 1 or x = 2 or x = 3 or x = 4 by A00,ENUMSET1:def 2;
     hence thesis by Q1,F2;
   end; then
   f2=f by E1;
   hence thesis by X1,B1,Q1;
   end;
   suppose SUPP1: i=3; then
   FunctionRV2(i,Sigma,f1,f2,f3) = FunctionRV1(i,Sigma,f1,f2,f3)
    by A0,A00,a0,F1,Def1212; then
x1:FunctionRV2(i,Sigma,f1,f2,f3) = f1 by a0,A0,A00,F2,F3,SUPP1,Def1211;
    60 in REAL & 80 in REAL & 100 in REAL & 120 in REAL by NUMBERS:19; then
    consider f being Function of Omega,REAL such that
     Q1: f.1=60 & f.2=80 & f.3=100 & f.4=120 &
       f is (El_Filtration(i,MyFunc),Borel_Sets)-random_variable-like
        by SUPP1,A00,A1,MyFunc5;
E1:dom f=Omega by FUNCT_2:def 1;
   for x being object st x in dom f holds f.x = f1.x
   proof
     let x be object;
     assume x in dom f;
     then reconsider x as Element of Omega;
     x = 1 or x = 2 or x = 3 or x = 4 by A00,ENUMSET1:def 2;
     hence thesis by Q1,F3;
   end; then
   f1=f by E1;
   hence thesis by x1,B1,Q1;
   end;
  end;
  hence thesis;
  end;
  for k being Element of I holds
            (ex RV being Function of Omega,REAL st
           (fI1.k=RV & RV is (Sigma,Borel_Sets)-random_variable-like &
         RV is (El_Filtration(k,MyFunc),Borel_Sets)-random_variable-like)) &
             (ex f being Function of Omega,REAL st
             k=1 implies f.1=100 & f.2=100 & f.3=100 & f.4=100 & fI1.k=f) &
          (ex f being Function of Omega,REAL st
         k=2 implies f.1=80 & f.2=80 & f.3=120 & f.4=120 & fI1.k=f) &
       (ex f being Function of Omega,REAL st
         k=3 implies f.1=60 & f.2=80 & f.3=100 & f.4=120 & fI1.k=f)
  proof
   let k be Element of I;
   consider RV being Function of Omega,REAL such that O1:
   fI1.k=RV & RV is (Sigma,Borel_Sets)-random_variable-like by Fin1;
o1: RV is (El_Filtration(k,MyFunc),Borel_Sets)-random_variable-like
    proof
     fI1.k=RVProcess(fI1,k) &
     RVProcess(fI1,k) is
       (El_Filtration(k,MyFunc),Borel_Sets)-random_variable-like
      by Fin3;
    hence thesis by O1;
    end;
   GFin2: ex f being Function of Omega,REAL st
          k=1 implies fI1.k=f & f.1=100 & f.2=100 & f.3=100 & f.4=100 & fI1.k=f
   proof
    k=1 implies fI1.k=f3
    proof
     assume K1: k=1;
     fI1.k=FunctionRV2(k,Sigma,f1,f2,f3) by B1;
     hence thesis by a0,A0,A00,F1,K1,Def1212;
    end;
   hence thesis by F1;
   end;
   GFin3: ex f being Function of Omega,REAL st
          k=2 implies fI1.k=f & f.1=80 & f.2=80 & f.3=120 & f.4=120 & fI1.k=f
   proof
    k=2 implies fI1.k=f2
    proof
     assume K1: k=2;
     fI1.k=FunctionRV2(k,Sigma,f1,f2,f3) by B1; then
     fI1.k=FunctionRV1(k,Sigma,f1,f2,f3) by a0,A0,A00,F1,K1,Def1212;
    hence thesis by a0,A0,A00,F2,F3,K1,Def1211;
    end;
   hence thesis by F2;
   end;
   ex f being Function of Omega,REAL st
      k=3 implies fI1.k=f & f.1=60 & f.2=80 & f.3=100 & f.4=120 & fI1.k=f
   proof
    k=3 implies fI1.k=f1
    proof
     assume K1: k=3;
     fI1.k=FunctionRV2(k,Sigma,f1,f2,f3) by B1;
     then fI1.k=FunctionRV1(k,Sigma,f1,f2,f3) by a0,A0,A00,F1,K1,Def1212;
    hence thesis by a0,A0,A00,F2,F3,K1,Def1211;
    end;
   hence thesis by F3;
   end;
   hence thesis by o1,O1,GFin2,GFin3;
  end;
  hence thesis by Fin3,Def30002;
  end;
  hence thesis;
 end;