set f = Omega1 --> the Element of Omega2;
reconsider f = Omega1 --> the Element of Omega2 as Function of Omega1,Omega2 ;
take f ; :: thesis: f is S1,S2 -random_variable-like
thus f is S1,S2 -random_variable-like by LemmaExample; :: thesis: verum