set M = the sigma_Measure of S;

set F = {1} --> the sigma_Measure of S;

for x being set st x in dom ({1} --> the sigma_Measure of S) holds

ex MM being sigma_Measure of S st ({1} --> the sigma_Measure of S) . x = MM by FUNCOP_1:7;

hence ex b_{1} being Function st b_{1} is S -Measure_valued
by Def3; :: thesis: verum

set F = {1} --> the sigma_Measure of S;

for x being set st x in dom ({1} --> the sigma_Measure of S) holds

ex MM being sigma_Measure of S st ({1} --> the sigma_Measure of S) . x = MM by FUNCOP_1:7;

hence ex b