let Omega, Omega2 be non empty set ; :: thesis:
let Sigma be SigmaField of Omega; :: thesis:
let Sigma2 be SigmaField of Omega2; :: thesis:
let I be non empty real-membered set ; :: thesis:
let Q be ManySortedSigmaField of I,Sigma; :: thesis:
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:
let i be Element of I; :: thesis:
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:
assume x in Sigma2 ; :: thesis:

per cases ;

suppose CAS0: w in x ; :: thesis:

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 Omega implies y in myfunc " x )

proof

assume I0: y in Omega ; :: thesis:
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:

end;

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

end;

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

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:

end;

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

end;

suppose CAS1: not w in x ; :: thesis:

myfunc " x c= {}

proof

let z be object ; :: according to TARSKI:def 3 :: thesis:
assume z in myfunc " x ; :: thesis:
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:

end;

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

end;

end;

end;

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

end;

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