let S be non empty finite set ; 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; 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; 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; 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 ; 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; ( F = dom s & E = trueEVENT (judgefunc * s) implies Prob (judgefunc,s) = prob E )
assume A1:
( F = dom s & E = trueEVENT (judgefunc * s) )
; 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; verum