:: deftheorem defines Finseq-EQclass DIST_1:def 5 :
for S being finite set
for s being FinSequence of S holds Finseq-EQclass s = { t where t is FinSequence of S : s,t -are_prob_equivalent } ;