let S be non empty finite set ; :: thesis: for D being EqSampleSpaces of S
for s being Element of D
for judgefunc being Function of S,BOOLEAN
for F being non empty finite set
for E being Event of F st F = dom s & E = trueEVENT (judgefunc * s) holds
Prob (judgefunc,s) = prob E
let D be EqSampleSpaces of S; :: thesis: for s being Element of D
for judgefunc being Function of S,BOOLEAN
for F being non empty finite set
for E being Event of F st F = dom s & E = trueEVENT (judgefunc * s) holds
Prob (judgefunc,s) = prob E
let s be Element of D; :: thesis: for judgefunc being Function of S,BOOLEAN
for F being non empty finite set
for E being Event of F st F = dom s & E = trueEVENT (judgefunc * s) holds
Prob (judgefunc,s) = prob E
let judgefunc be Function of S,BOOLEAN; :: thesis: for F being non empty finite set
for E being Event of F st F = dom s & E = trueEVENT (judgefunc * s) holds
Prob (judgefunc,s) = prob E
let F be non empty finite set ; :: thesis: for E being Event of F st F = dom s & E = trueEVENT (judgefunc * s) holds
Prob (judgefunc,s) = prob E
let E be Event of F; :: thesis: ( F = dom s & E = trueEVENT (judgefunc * s) implies Prob (judgefunc,s) = prob E )
assume A1: ( F = dom s & E = trueEVENT (judgefunc * s) ) ; :: thesis: Prob (judgefunc,s) = prob E
then card F = card (Seg (len s)) by FINSEQ_1:def 3
.= len s by FINSEQ_1:57 ;
hence Prob (judgefunc,s) = prob E by A1; :: thesis: verum