let S be non empty finite set ; :: thesis: for p being distProbFinS of S holds
( distribution (p,S) is Element of distribution_family S & (GenProbSEQ S) . (distribution (p,S)) = p )
let p be distProbFinS of S; :: 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
ex s being FinSequence of S st FDprobSEQ s = p by Def10;
hence (GenProbSEQ S) . (distribution (p,S)) = p by Def8; :: thesis: verum