for S being non empty finite set
for p being distProbFinS of S holds
( distribution (p,S) is Element of distribution_family S & (GenProbSEQ S) . (distribution (p,S)) = p )