let S be non empty finite set ; :: thesis: for D being EqSampleSpaces of S
for x being sample of D holds Prob x = (ProbFinS_of D) . (index x)
let D be EqSampleSpaces of S; :: thesis: for x being sample of D holds Prob x = (ProbFinS_of D) . (index x)
let x be sample of D; :: thesis: Prob x = (ProbFinS_of D) . (index x)
reconsider f = chi ({x},S) as Element of Funcs (S,BOOLEAN) by FUNCT_2:8, MARGREL1:def 11;
set s = the Element of D;
A1: for a being set st a = x holds
f . a = TRUE
proof
let a be set ; :: thesis: ( a = x implies f . a = TRUE )
assume a = x ; :: thesis: f . a = TRUE
then a in {x} by TARSKI:def 1;
hence f . a = TRUE by FUNCT_3:def 3; :: thesis: verum
end;
for a being set st f . a = TRUE holds
a = x
proof
let a be set ; :: thesis: ( f . a = TRUE implies a = x )
assume f . a = TRUE ; :: thesis: a = x
then a in {x} by FUNCT_3:36;
hence a = x by TARSKI:def 1; :: thesis: verum
end;
then A2: Prob (f, the Element of D) = FDprobability (x, the Element of D) by Th10, A1;
A3: Prob x = FDprobability (x, the Element of D) by A2, Def6;
consider t being FinSequence of S such that
A4: ( t in D & (GenProbSEQ S) . D = FDprobSEQ t ) by DIST_1:def 7;
A5: (GenProbSEQ S) . D = FDprobSEQ the Element of D by A4, DIST_1:10, Th4;
reconsider n = x .. (canFS S) as Nat ;
len (canFS S) = card S by FINSEQ_1:93;
then A6: dom (canFS S) = Seg (card S) by FINSEQ_1:def 3;
A7: x in rng (canFS S) by Th3;
then n in dom (canFS S) by FINSEQ_4:20;
then A8: n in dom (FDprobSEQ the Element of D) by A6, DIST_1:def 3;
(canFS S) . n = x by A7, FINSEQ_4:19;
hence Prob x = (ProbFinS_of D) . (index x) by A3, A5, A8, DIST_1:def 3; :: thesis: verum