set Omega1 = the non empty set ;

set S1 = the SigmaField of the non empty set ;

set M = the random_variable of the SigmaField of the non empty set , the SigmaField of the non empty set ;

set F = {1} --> the random_variable of the SigmaField of the non empty set , the SigmaField of the non empty set ;

for x being set st x in dom ({1} --> the random_variable of the SigmaField of the non empty set , the SigmaField of the non empty set ) holds

ex Omega1, Omega2 being non empty set ex S1 being SigmaField of Omega1 ex S2 being SigmaField of Omega2 ex f being random_variable of S1,S2 st ({1} --> the random_variable of the SigmaField of the non empty set , the SigmaField of the non empty set ) . x = f by FUNCOP_1:7;

hence ex b_{1} being Function st b_{1} is random_variable_family-like
by Def2; :: thesis: verum

set S1 = the SigmaField of the non empty set ;

set M = the random_variable of the SigmaField of the non empty set , the SigmaField of the non empty set ;

set F = {1} --> the random_variable of the SigmaField of the non empty set , the SigmaField of the non empty set ;

for x being set st x in dom ({1} --> the random_variable of the SigmaField of the non empty set , the SigmaField of the non empty set ) holds

ex Omega1, Omega2 being non empty set ex S1 being SigmaField of Omega1 ex S2 being SigmaField of Omega2 ex f being random_variable of S1,S2 st ({1} --> the random_variable of the SigmaField of the non empty set , the SigmaField of the non empty set ) . x = f by FUNCOP_1:7;

hence ex b