:: deftheorem defines -are_prob_equivalent DIST_1:def 4 :

for S being finite set

for s, t being FinSequence of S holds

( s,t -are_prob_equivalent iff for x being set holds FDprobability (x,s) = FDprobability (x,t) );

for S being finite set

for s, t being FinSequence of S holds

( s,t -are_prob_equivalent iff for x being set holds FDprobability (x,s) = FDprobability (x,t) );