let Omega, Omega2 be non empty set ; :: thesis: for Sigma being SigmaField of Omega
for Sigma2 being SigmaField of Omega2
for I being non empty real-membered set
for Q being ManySortedSigmaField of I,Sigma 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
let Sigma be SigmaField of Omega; :: thesis: for Sigma2 being SigmaField of Omega2
for I being non empty real-membered set
for Q being ManySortedSigmaField of I,Sigma 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
let Sigma2 be SigmaField of Omega2; :: thesis: for I being non empty real-membered set
for Q being ManySortedSigmaField of I,Sigma 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
let I be non empty real-membered set ; :: thesis: for Q being ManySortedSigmaField of I,Sigma 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
let Q be ManySortedSigmaField of I,Sigma; :: thesis: 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
consider w being object such that
A00: w in Omega2 by XBOOLE_0:def 1;
reconsider w = w as Element of Omega2 by A00;
set myset = w;
deffunc H₁( Element of Omega) -> Element of Omega2 = w;
consider myfunc being Function of Omega,Omega2 such that
B3: myfunc = Omega --> w ;
take myfunc ; :: thesis: for i being Element of I holds myfunc is random_variable of El_Filtration (i,Q),Sigma2
let i be Element of I; :: thesis: myfunc is random_variable of El_Filtration (i,Q),Sigma2
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 ; :: thesis: ( x in Sigma2 implies myfunc " x in El_Filtration (i,Q) )
assume x in Sigma2 ; :: thesis: myfunc " x in El_Filtration (i,Q)

per cases ( w in x or not w in x ) ;

suppose CAS0: w in x ; :: thesis: myfunc " x in El_Filtration (i,Q)

H1: myfunc " x = Omega

proof

for y being object holds
( y in myfunc " x iff y in Omega )

proof

let y be object ; :: thesis: ( y in myfunc " x iff y in Omega )
( y in Omega implies y in myfunc " x )

proof

assume I0: y in Omega ; :: thesis: y in myfunc " x
then I1: y in dom myfunc by FUNCT_2:def 1;
myfunc . y in x by I0, B3, FUNCOP_1:7, CAS0;
hence y in myfunc " x by I1, FUNCT_1:def 7; :: thesis: verum

end;

hence ( y in myfunc " x iff y in Omega ) ; :: thesis: verum

end;

hence myfunc " x = Omega by TARSKI:def 3; :: thesis: verum

end;

myfunc " x in Q . i

proof

Q . i is SigmaField of Omega by KOLMOG01:def 2;
hence myfunc " x in Q . i by H1, PROB_1:5; :: thesis: verum

end;

hence myfunc " x in El_Filtration (i,Q) ; :: thesis: verum

end;

suppose CAS1: not w in x ; :: thesis: myfunc " x in El_Filtration (i,Q)

myfunc " x c= {}

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in myfunc " x or z in {} )
assume z in myfunc " x ; :: thesis: z in {}
then ( z in dom myfunc & myfunc . z in x & myfunc . z = w ) by FUNCT_1:def 7, B3, FUNCOP_1:7;
hence z in {} by CAS1; :: thesis: verum

end;

then myfunc " x = {} ;
hence myfunc " x in El_Filtration (i,Q) by PROB_1:4; :: thesis: verum

end;

end;

end;

hence myfunc is El_Filtration (i,Q),Sigma2 -random_variable-like ; :: thesis: verum

end;

hence myfunc is random_variable of El_Filtration (i,Q),Sigma2 ; :: thesis: verum