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

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