let F be Function; :: thesis: ( F is S -Probability_valued implies F is S -Measure_valued )

assume A1: F is S -Probability_valued ; :: thesis: F is S -Measure_valued

let y be set ; :: according to RANDOM_3:def 3 :: thesis: ( y in dom F implies ex M being sigma_Measure of S st F . y = M )

assume y in dom F ; :: thesis: ex M being sigma_Measure of S st F . y = M

then consider P being Probability of S such that

A2: F . y = P by A1;

take P2M P ; :: thesis: F . y = P2M P

thus F . y = P2M P by A2; :: thesis: verum

assume A1: F is S -Probability_valued ; :: thesis: F is S -Measure_valued

let y be set ; :: according to RANDOM_3:def 3 :: thesis: ( y in dom F implies ex M being sigma_Measure of S st F . y = M )

assume y in dom F ; :: thesis: ex M being sigma_Measure of S st F . y = M

then consider P being Probability of S such that

A2: F . y = P by A1;

take P2M P ; :: thesis: F . y = P2M P

thus F . y = P2M P by A2; :: thesis: verum