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 S1,S2 -random_variable-like ) ;
hence ex b₁ being Function of Omega1,Omega2 st b₁ is S1,S2 -random_variable-like ; :: thesis: verum