for S being finite set
for s, t being FinSequence of S st t in Finseq-EQclass s holds
FDprobSEQ s = FDprobSEQ t