let S be finite set ; :: thesis: for s, t being FinSequence of S st t in Finseq-EQclass s holds

FDprobSEQ s = FDprobSEQ t

let s, t be FinSequence of S; :: thesis: ( t in Finseq-EQclass s implies FDprobSEQ s = FDprobSEQ t )

assume t in Finseq-EQclass s ; :: thesis: FDprobSEQ s = FDprobSEQ t

then ex w being FinSequence of S st

( t = w & s,w -are_prob_equivalent ) ;

hence FDprobSEQ s = FDprobSEQ t by Th8; :: thesis: verum

FDprobSEQ s = FDprobSEQ t

let s, t be FinSequence of S; :: thesis: ( t in Finseq-EQclass s implies FDprobSEQ s = FDprobSEQ t )

assume t in Finseq-EQclass s ; :: thesis: FDprobSEQ s = FDprobSEQ t

then ex w being FinSequence of S st

( t = w & s,w -are_prob_equivalent ) ;

hence FDprobSEQ s = FDprobSEQ t by Th8; :: thesis: verum