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

( 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