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;

for s being FinSequence of S

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