let S be non empty finite set ; :: thesis: for D being EqSampleSpaces of S
for a being Element of S
for s being Element of D
for judgefunc being Function of S,BOOLEAN st ( for x being set holds
( x = a iff judgefunc . x = TRUE ) ) holds
Prob (judgefunc,s) = FDprobability (a,s)
let D be EqSampleSpaces of S; :: thesis: for a being Element of S
for s being Element of D
for judgefunc being Function of S,BOOLEAN st ( for x being set holds
( x = a iff judgefunc . x = TRUE ) ) holds
Prob (judgefunc,s) = FDprobability (a,s)
let a be Element of S; :: thesis: for s being Element of D
for judgefunc being Function of S,BOOLEAN st ( for x being set holds
( x = a iff judgefunc . x = TRUE ) ) holds
Prob (judgefunc,s) = FDprobability (a,s)
let s be Element of D; :: thesis: for judgefunc being Function of S,BOOLEAN st ( for x being set holds
( x = a iff judgefunc . x = TRUE ) ) holds
Prob (judgefunc,s) = FDprobability (a,s)
let judgefunc be Function of S,BOOLEAN; :: thesis: ( ( for x being set holds
( x = a iff judgefunc . x = TRUE ) ) implies Prob (judgefunc,s) = FDprobability (a,s) )
assume A1: for x being set holds
( x = a iff judgefunc . x = TRUE ) ; :: thesis: Prob (judgefunc,s) = FDprobability (a,s)
A2: for n being set holds
( n in s " {a} iff ( n in dom s & s . n = a ) )

proof

let n be set ; :: thesis: ( n in s " {a} iff ( n in dom s & s . n = a ) )
( n in s " {a} iff ( n in dom s & s . n in {a} ) ) by FUNCT_1:def 7;
hence ( n in s " {a} iff ( n in dom s & s . n = a ) ) by TARSKI:def 1; :: thesis: verum

end;

A3: for x being object st x in (judgefunc * s) " {TRUE} holds
x in s " {a}

proof

let x be object ; :: thesis: ( x in (judgefunc * s) " {TRUE} implies x in s " {a} )
assume x in (judgefunc * s) " {TRUE} ; :: thesis: x in s " {a}
then A4: ( x in dom (judgefunc * s) & (judgefunc * s) . x in {TRUE} ) by FUNCT_1:def 7;
then (judgefunc * s) . x = TRUE by TARSKI:def 1;
then A5: ( x in dom s & judgefunc . (s . x) = TRUE ) by A4, FUNCT_1:11, FUNCT_1:12;
then s . x = a by A1;
then s . x in {a} by TARSKI:def 1;
hence x in s " {a} by A5, FUNCT_1:def 7; :: thesis: verum

end;

for x being object st x in s " {a} holds
x in (judgefunc * s) " {TRUE}

proof

let x be object ; :: thesis: ( x in s " {a} implies x in (judgefunc * s) " {TRUE} )
assume A6: x in s " {a} ; :: thesis: x in (judgefunc * s) " {TRUE}
then A7: ( x in dom s & s . x = a ) by A2;
s . x in S by A7;
then A8: s . x in dom judgefunc by FUNCT_2:def 1;
judgefunc . (s . x) = TRUE by A6, A2, A1;
then (judgefunc * s) . x = TRUE by A6, A2, FUNCT_1:13;
then A9: (judgefunc * s) . x in {TRUE} by TARSKI:def 1;
x in dom (judgefunc * s) by A7, A8, FUNCT_1:11;
hence x in (judgefunc * s) " {TRUE} by A9, FUNCT_1:def 7; :: thesis: verum

end;

hence Prob (judgefunc,s) = FDprobability (a,s) by A3, TARSKI:2; :: thesis: verum