let S be non empty finite set ; :: thesis: for p being distProbFinS of S holds
( p is ProbFinS FinSequence of REAL & len p = card S & ex s being FinSequence of S st FDprobSEQ s = p & distribution (p,S) is Element of distribution_family S & (GenProbSEQ S) . (distribution (p,S)) = p )
let p be distProbFinS of S; :: thesis: ( p is ProbFinS FinSequence of REAL & len p = card S & ex s being FinSequence of S st FDprobSEQ s = p & distribution (p,S) is Element of distribution_family S & (GenProbSEQ S) . (distribution (p,S)) = p )
thus p is ProbFinS FinSequence of REAL ; :: thesis: ( len p = card S & ex s being FinSequence of S st FDprobSEQ s = p & distribution (p,S) is Element of distribution_family S & (GenProbSEQ S) . (distribution (p,S)) = p )
thus A1: ( len p = card S & ex s being FinSequence of S st FDprobSEQ s = p ) by Def10; :: thesis: ( distribution (p,S) is Element of distribution_family S & (GenProbSEQ S) . (distribution (p,S)) = p )
thus distribution (p,S) is Element of distribution_family S ; :: thesis: (GenProbSEQ S) . (distribution (p,S)) = p
thus (GenProbSEQ S) . (distribution (p,S)) = p by A1, Def8; :: thesis: verum