for Omega, Omega2 being non empty set
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