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₁ being Function st b₁ is random_variable_family-like by Def2; :: thesis: verum