let Omega1, Omega2 be non empty set ; :: thesis: for F being Function of Omega1,Omega2 holds F is random_variable of Trivial-SigmaField Omega1, Trivial-SigmaField Omega2
let F be Function of Omega1,Omega2; :: thesis: F is random_variable of Trivial-SigmaField Omega1, Trivial-SigmaField Omega2
set S1 = Trivial-SigmaField Omega1;
set S2 = Trivial-SigmaField Omega2;
for y being set st y in Trivial-SigmaField Omega2 holds
F " y in Trivial-SigmaField Omega1 ;
hence F is random_variable of Trivial-SigmaField Omega1, Trivial-SigmaField Omega2 by FINANCE1:def 5; :: thesis: verum