theorem :: DIST_2:1

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