let Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega
for P, P1 being Probability of Sigma st ( for A being Event of Sigma holds P . A = P1 . A ) holds
P = P1
let Sigma be SigmaField of Omega; :: thesis: for P, P1 being Probability of Sigma st ( for A being Event of Sigma holds P . A = P1 . A ) holds
P = P1
let P, P1 be Probability of Sigma; :: thesis: ( ( for A being Event of Sigma holds P . A = P1 . A ) implies P = P1 )
assume for A being Event of Sigma holds P . A = P1 . A ; :: thesis: P = P1
then for x being object st x in Sigma holds
P . x = P1 . x ;
hence P = P1 by FUNCT_2:12; :: thesis: verum