let Omega, Omega2 be non empty set ; :: thesis: for F being SigmaField of Omega
for F2 being SigmaField of Omega2
for k being Element of set_of_random_variables_on (F,F2) holds Change_Element_to_Func (F,F2,k) is random_variable of F,F2
let F be SigmaField of Omega; :: thesis: for F2 being SigmaField of Omega2
for k being Element of set_of_random_variables_on (F,F2) holds Change_Element_to_Func (F,F2,k) is random_variable of F,F2
let F2 be SigmaField of Omega2; :: thesis: for k being Element of set_of_random_variables_on (F,F2) holds Change_Element_to_Func (F,F2,k) is random_variable of F,F2
let k be Element of set_of_random_variables_on (F,F2); :: thesis: Change_Element_to_Func (F,F2,k) is random_variable of F,F2
Change_Element_to_Func (F,F2,k) is Element of { f where f is Function of Omega,Omega2 : f is_random_variable_on F,F2 } by FINANCE1:def 7;
then Change_Element_to_Func (F,F2,k) in { f where f is Function of Omega,Omega2 : f is_random_variable_on F,F2 } ;
then ex Y being Function of Omega,Omega2 st
( Change_Element_to_Func (F,F2,k) = Y & Y is_random_variable_on F,F2 ) ;
hence Change_Element_to_Func (F,F2,k) is random_variable of F,F2 by RANDOM_3:def 1; :: thesis: verum