let S be non empty finite set ; :: thesis: 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; :: thesis: for f being Function of S,BOOLEAN st f = chi (S,S) holds
Prob (f,D) = 1
let f be Function of S,BOOLEAN; :: thesis: ( f = chi (S,S) implies Prob (f,D) = 1 )
assume A1: f = chi (S,S) ; :: thesis: 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 ; :: thesis: verum