let S be non empty finite set ; :: thesis: for p being distProbFinS of S
for s being FinSequence of S st FDprobSEQ s = p holds
( distribution (p,S) = Finseq-EQclass s & s in distribution (p,S) )
let p be distProbFinS of S; :: thesis: for s being FinSequence of S st FDprobSEQ s = p holds
( distribution (p,S) = Finseq-EQclass s & s in distribution (p,S) )
let s be FinSequence of S; :: thesis: ( FDprobSEQ s = p implies ( distribution (p,S) = Finseq-EQclass s & s in distribution (p,S) ) )
assume A1: FDprobSEQ s = p ; :: thesis: ( distribution (p,S) = Finseq-EQclass s & s in distribution (p,S) )
set D = Finseq-EQclass s;
reconsider D = Finseq-EQclass s as Element of distribution_family S by DIST_1:def 6;
(GenProbSEQ S) . (Finseq-EQclass s) = p by A1, DIST_1:12;
then D = distribution (p,S) by A1, DIST_1:def 8;
hence ( distribution (p,S) = Finseq-EQclass s & s in distribution (p,S) ) ; :: thesis: verum