let S be non empty finite set ; :: thesis: for D being Element of distribution_family S
for s, t being Element of D holds s,t -are_prob_equivalent
let D be Element of distribution_family S; :: thesis: for s, t being Element of D holds s,t -are_prob_equivalent
let s, t be Element of D; :: thesis: s,t -are_prob_equivalent
consider x being FinSequence of S such that
A1: D = Finseq-EQclass x by DIST_1:def 6;
( s,x -are_prob_equivalent & x,t -are_prob_equivalent ) by A1, DIST_1:7;
hence s,t -are_prob_equivalent by DIST_1:6; :: thesis: verum