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 A1, 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 } by A1;
then consider Y being Function of Omega,Omega2 such that
A1: ( Change_Element_to_Func (F,F2,k) = Y & Y is_random_variable_on F,F2 ) ;
thus Change_Element_to_Func (F,F2,k) is random_variable of F,F2 by A1, RANDOM_3:def 1; :: thesis: verum