let S be non empty finite set ; for D being EqSampleSpaces of S
for f being Function of S,BOOLEAN st f = chi (S,S) holds
Prob (f,D) = 1
let D be EqSampleSpaces of S; for f being Function of S,BOOLEAN st f = chi (S,S) holds
Prob (f,D) = 1
let f be Function of S,BOOLEAN; ( f = chi (S,S) implies Prob (f,D) = 1 )
assume A1:
f = chi (S,S)
; Prob (f,D) = 1
set s = the Element of D;
reconsider s0 = dom the Element of D as finite set ;
reconsider CfS = Coim ((f * the Element of D),TRUE) as finite set ;
card (Seg (len the Element of D)) = len the Element of D
by FINSEQ_1:57;
then A2:
card s0 = len the Element of D
by FINSEQ_1:def 3;
A3:
the Element of D is Function of (dom the Element of D),(rng the Element of D)
by FUNCT_2:1;
A4:
the Element of D is Function of (dom the Element of D),S
by A3, FUNCT_2:2;
A5:
f is Function of (dom f),(rng f)
by FUNCT_2:1;
S c= S
;
then A6:
f is Function of (dom f),{TRUE}
by A5, A1, INTEGRA1:17;
A7:
dom f = S
by FUNCT_2:def 1;
A8: trueEVENT (f * the Element of D) =
the Element of D " (trueEVENT f)
by Th14
.=
the Element of D " S
by A7, A6, FUNCT_2:40
.=
dom the Element of D
by A4, FUNCT_2:40
;
thus Prob (f,D) =
Prob (f, the Element of D)
by Def6
.=
1
by A2, A8, XCMPLX_1:60
; verum