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

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