theorem :: DIST_1:5

for S being finite set
for s being FinSequence of S
for x being set holds FDprobability (x,s) = prob (event_pick (x,s)) by CARD_1:62;