for Y being non empty finite set
for s being FinSequence of Y st Y = {1} & s = <*1*> holds
FDprobSEQ s = <*1*>