let S be 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 Def6;
then consider u being FinSequence of S such that
A1: u in Finseq-EQclass s and
A2: (GenProbSEQ S) . (Finseq-EQclass s) = FDprobSEQ u by Def7;
s,u -are_prob_equivalent by A1, Th5;
hence (GenProbSEQ S) . (Finseq-EQclass s) = FDprobSEQ s by A2, Th8; :: thesis: verum