set M = the Real-Valued-Random-Variable of S;

set F = {1} --> the Real-Valued-Random-Variable of S;

for x being set st x in dom ({1} --> the Real-Valued-Random-Variable of S) holds

ex Z being Real-Valued-Random-Variable of S st ({1} --> the Real-Valued-Random-Variable of S) . x = Z by FUNCOP_1:7;

hence ex b_{1} being Function st b_{1} is S -Random-Variable-Family
by Def5; :: thesis: verum

set F = {1} --> the Real-Valued-Random-Variable of S;

for x being set st x in dom ({1} --> the Real-Valued-Random-Variable of S) holds

ex Z being Real-Valued-Random-Variable of S st ({1} --> the Real-Valued-Random-Variable of S) . x = Z by FUNCOP_1:7;

hence ex b