let S be non empty finite set ; 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; for x being sample of D holds Prob x = (ProbFinS_of D) . (index x)
let x be sample of D; 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
for a being set st f . a = TRUE holds
a = x
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; verum