:: 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 } ;

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 } ;