let X, Y be non empty set ; :: thesis: for S being SigmaField of Y
for M being Probability of S holds X --> M is S -Probability_valued
let S be SigmaField of Y; :: thesis: for M being Probability of S holds X --> M is S -Probability_valued
let M be Probability of S; :: thesis: X --> M is S -Probability_valued
set F = X --> M;
for x being set st x in dom (X --> M) holds
ex P being Probability of S st (X --> M) . x = P by FUNCOP_1:7;
hence X --> M is S -Probability_valued ; :: thesis: verum