let S be non empty finite set ; :: thesis: for s being FinSequence of S holds (GenProbSEQ S) . (Finseq-EQclass s) = FDprobSEQ s
let s be FinSequence of S; :: thesis: (GenProbSEQ S) . (Finseq-EQclass s) = FDprobSEQ s
Finseq-EQclass s is Element of distribution_family S by defQuot;
then consider u being FinSequence of S such that
P2: ( u in Finseq-EQclass s & (GenProbSEQ S) . (Finseq-EQclass s) = FDprobSEQ u ) by defFREQDIST2;
s,u -are_prob_equivalent by P2, EQX02;
hence (GenProbSEQ S) . (Finseq-EQclass s) = FDprobSEQ s by P2, EQX05; :: thesis: verum