let Omega, Omega2 be non empty set ; :: thesis:
assume A00: Omega = {1,2,3,4} ; :: thesis:
let Sigma be SigmaField of Omega; :: thesis:
let I be non empty real-membered set ; :: thesis:
assume that
A0: I = {1,2,3} and
a0: Sigma = bool {1,2,3,4} ; :: thesis:
let MyFunc be Filtration of I,Sigma; :: thesis:
assume A1: ( MyFunc . 1 = Special_SigmaField1 & MyFunc . 2 = Special_SigmaField2 & MyFunc . 3 = Trivial-SigmaField {1,2,3,4} ) ; :: thesis:
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 H₁( Element of I) -> Element of set_of_random_variables_on (Sigma,Borel_Sets) = 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 being Element of I holds fI1 . d = H₁(d) from FUNCT_2:sch 4();
Fin1: for k being Element of I ex RV being Function of Omega,REAL st
( fI1 . k = RV & RV is Sigma, Borel_Sets -random_variable-like )

let k be Element of I; :: thesis:
fI1 . k in set_of_random_variables_on (Sigma,Borel_Sets) ;
hence ex RV being Function of Omega,REAL st
( fI1 . k = RV & RV is Sigma, Borel_Sets -random_variable-like ) ; :: thesis:

end;

then reconsider fI1 = fI1 as Stochastic_Process of I,Sigma, Borel_Sets by Def30000;
take fI1 ; :: thesis:
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; :: thesis:
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; :: thesis:

per cases by A0, ENUMSET1:def 1;

suppose SUPP: i = 1 ; :: thesis:

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 ; :: thesis:
assume x in dom f ; :: thesis:
then reconsider x = x as Element of Omega ;
( x = 1 or x = 2 or x = 3 or x = 4 ) by A00, ENUMSET1:def 2;
hence f . x = f3 . x by Q1, F1; :: thesis:

end;

then f3 = f by E1;
hence RVProcess (fI1,i) is El_Filtration (i,MyFunc), Borel_Sets -random_variable-like by X1, B1, Q1; :: thesis:

end;

suppose SUPP2: i = 2 ; :: thesis:

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 ; :: thesis:
assume x in dom f ; :: thesis:
then reconsider x = x as Element of Omega ;
( x = 1 or x = 2 or x = 3 or x = 4 ) by A00, ENUMSET1:def 2;
hence f . x = f2 . x by Q1, F2; :: thesis:

end;

then f2 = f by E1;
hence RVProcess (fI1,i) is El_Filtration (i,MyFunc), Borel_Sets -random_variable-like by X1, B1, Q1; :: thesis:

end;

suppose SUPP1: i = 3 ; :: thesis:

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 ; :: thesis:
assume x in dom f ; :: thesis:
then reconsider x = x as Element of Omega ;
( x = 1 or x = 2 or x = 3 or x = 4 ) by A00, ENUMSET1:def 2;
hence f . x = f1 . x by Q1, F3; :: thesis:

end;

then f1 = f by E1;
hence RVProcess (fI1,i) is El_Filtration (i,MyFunc), Borel_Sets -random_variable-like by x1, B1, Q1; :: thesis:

end;

hence fI1 is MyFunc -stoch_proc_wrt_to_Filtration ; :: 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; :: thesis:
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 RV is El_Filtration (k,MyFunc), Borel_Sets -random_variable-like by O1; :: thesis:

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 ; :: thesis:
fI1 . k = FunctionRV2 (k,Sigma,f1,f2,f3) by B1;
hence fI1 . k = f3 by a0, A0, A00, F1, K1, Def1212; :: thesis:

end;

hence 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 ) ) by F1; :: thesis:

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 ; :: thesis:
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 fI1 . k = f2 by a0, A0, A00, F2, F3, K1, Def1211; :: thesis:

end;

hence 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 ) ) by F2; :: thesis:

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 ; :: thesis:
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 fI1 . k = f1 by a0, A0, A00, F2, F3, K1, Def1211; :: thesis:

end;

hence 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 ) ) by F3; :: thesis:

end;

hence ( 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 ) ) ) by o1, O1, GFin2, GFin3; :: thesis:

end;

hence ( ( 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 ) ; :: thesis: