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