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

now :: thesis: ( t in Finseq-EQclass s implies s,t -are_prob_equivalent )

assume t in Finseq-EQclass s ; :: thesis: s,t -are_prob_equivalent
then ex t0 being FinSequence of S st
( t = t0 & s,t0 -are_prob_equivalent ) ;
hence s,t -are_prob_equivalent ; :: thesis: verum

end;

hence ( s,t -are_prob_equivalent iff t in Finseq-EQclass s ) ; :: thesis: verum