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 Subset of REAL; :: thesis:
let Q be Filtration 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 ;
B4: for i being Element of I holds myfunc is random_variable of Sigma_of_ManySortedSigmaField (Q,i),Sigma2

proof

let i be Element of I; :: thesis:
myfunc is_random_variable_on Sigma_of_ManySortedSigmaField (Q,i),Sigma2

proof

for x being set st x in Sigma2 holds
myfunc " x in Sigma_of_ManySortedSigmaField (Q,i)

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 Sigma_of_ManySortedSigmaField (Q,i) ; :: thesis:

end;

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

myfunc " x = {}

proof

for z being object holds
( z in myfunc " x iff z in {} )

proof

let z be object ; :: thesis:
thus ( z in myfunc " x implies z in {} ) :: thesis:

proof

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;

thus ( z in {} implies z in myfunc " x ) ; :: thesis:

end;

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

end;

hence myfunc " x in Sigma_of_ManySortedSigmaField (Q,i) by PROB_1:4; :: thesis:

end;

end;

end;

hence myfunc is_random_variable_on Sigma_of_ManySortedSigmaField (Q,i),Sigma2 ; :: thesis:

end;

hence myfunc is random_variable of Sigma_of_ManySortedSigmaField (Q,i),Sigma2 by RANDOM_3:def 1; :: thesis:

end;

take myfunc ; :: thesis:
thus for i being Element of I holds myfunc is random_variable of Sigma_of_ManySortedSigmaField (Q,i),Sigma2 by B4; :: thesis: