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

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