set F = the Element of set_of_random_variables_on (S1,S2);
the Element of set_of_random_variables_on (S1,S2) in set_of_random_variables_on (S1,S2) ;
then ex f being Function of Omega1,Omega2 st
( the Element of set_of_random_variables_on (S1,S2) = f & f is_random_variable_on S1,S2 ) ;
hence ex b₁ being Function of Omega1,Omega2 st b₁ is S1,S2 -random_variable-like by Def1; :: thesis: verum