let S be non empty finite set ; :: thesis: for s, t, u being FinSequence of S st s,t -are_prob_equivalent & t,u -are_prob_equivalent holds
s,u -are_prob_equivalent
let s, t, u be FinSequence of S; :: thesis: ( s,t -are_prob_equivalent & t,u -are_prob_equivalent implies s,u -are_prob_equivalent )
assume that
A1: s,t -are_prob_equivalent and
A2: t,u -are_prob_equivalent ; :: thesis: s,u -are_prob_equivalent

now

let x be set ; :: thesis: FDprobability (x,s) = FDprobability (x,u)
thus FDprobability (x,s) = FDprobability (x,t) by A1, Def4
.= FDprobability (x,u) by A2, Def4 ; :: thesis: verum

end;

hence s,u -are_prob_equivalent by Def4; :: thesis: verum