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

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