set q = the Element of Omega2;
set F = Omega --> the Element of Omega2;
A1: Omega --> the Element of Omega2 is Sigma,Sigma2 -random_variable-like by 1A5;
Omega --> the Element of Omega2 in set_of_random_variables_on (Sigma,Sigma2) by A1;
then reconsider F = Omega --> the Element of Omega2 as Element of set_of_random_variables_on (Sigma,Sigma2) ;
deffunc H₁( Element of I) -> Element of set_of_random_variables_on (Sigma,Sigma2) = F;
consider fI1 being Function of I,(set_of_random_variables_on (Sigma,Sigma2)) such that
B1: for d being Element of I holds fI1 . d = H₁(d) from FUNCT_2:sch 4();
for k being Element of I ex RV being Function of Omega,Omega2 st
( fI1 . k = RV & RV is Sigma,Sigma2 -random_variable-like ) by A1, B1;
hence ex b₁ being Function of I,(set_of_random_variables_on (Sigma,Sigma2)) st
for k being Element of I ex RV being Function of Omega,Omega2 st
( b₁ . k = RV & RV is Sigma,Sigma2 -random_variable-like ) ; :: thesis: verum