set M = the Probability of S;
set F = {1} --> the Probability of S;
for x being set st x in dom ({1} --> the Probability of S) holds
ex P being Probability of S st ({1} --> the Probability of S) . x = P by FUNCOP_1:7;
hence ex b₁ being Function st b₁ is S -Probability_valued by Def4; :: thesis: verum