let F, G be Probability of Trivial-SigmaField S; :: thesis: ( ( for x being set st x in Trivial-SigmaField S holds
ex ch being Function of S,BOOLEAN st
( ch = chi (x,S) & F . x = Prob (ch,D) ) ) & ( for x being set st x in Trivial-SigmaField S holds
ex ch being Function of S,BOOLEAN st
( ch = chi (x,S) & G . x = Prob (ch,D) ) ) implies F = G )
assume A1: for A being set st A in Trivial-SigmaField S holds
ex ch being Function of S,BOOLEAN st
( ch = chi (A,S) & F . A = Prob (ch,D) ) ; :: thesis: ( ex x being set st
( x in Trivial-SigmaField S & ( for ch being Function of S,BOOLEAN holds
( not ch = chi (x,S) or not G . x = Prob (ch,D) ) ) ) or F = G )
assume A2: for A being set st A in Trivial-SigmaField S holds
ex ch being Function of S,BOOLEAN st
( ch = chi (A,S) & G . A = Prob (ch,D) ) ; :: thesis: F = G
now :: thesis: for x being object st x in Trivial-SigmaField S holds
F . x = G . x
let x be object ; :: thesis: ( x in Trivial-SigmaField S implies F . x = G . x )
assume A3: x in Trivial-SigmaField S ; :: thesis: F . x = G . x
reconsider X = x as set by TARSKI:1;
consider ch1 being Function of S,BOOLEAN such that
A4: ( ch1 = chi (X,S) & F . x = Prob (ch1,D) ) by A1, A3;
consider ch2 being Function of S,BOOLEAN such that
A5: ( ch2 = chi (X,S) & G . x = Prob (ch2,D) ) by A3, A2;
thus F . x = G . x by A4, A5; :: thesis: verum
end;
hence F = G by FUNCT_2:12; :: thesis: verum