:: 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) );