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