let S be finite set ; :: thesis: for s, t being FinSequence of S st t in Finseq-EQclass s holds
FDprobSEQ s = FDprobSEQ t
let s, t be FinSequence of S; :: thesis: ( t in Finseq-EQclass s implies FDprobSEQ s = FDprobSEQ t )
assume t in Finseq-EQclass s ; :: thesis: FDprobSEQ s = FDprobSEQ t
then ex w being FinSequence of S st
( t = w & s,w -are_prob_equivalent ) ;
hence FDprobSEQ s = FDprobSEQ t by Th8; :: thesis: verum