:: deftheorem Def3 defines FDprobSEQ DIST_1:def 3 :
for S being finite set
for s being FinSequence of S
for b₃ being FinSequence of REAL holds
( b₃ = FDprobSEQ s iff ( dom b₃ = Seg (card S) & ( for n being Nat st n in dom b₃ holds
b₃ . n = FDprobability (((canFS S) . n),s) ) ) );