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

A1: now

assume A2: s,t -are_prob_equivalent ; :: thesis: Finseq-EQclass t = Finseq-EQclass s

now

let x be set ; :: thesis: ( x in Finseq-EQclass t implies x in Finseq-EQclass s )
assume x in Finseq-EQclass t ; :: thesis: x in Finseq-EQclass s
then consider u being FinSequence of S such that
A3: x = u and
A4: t,u -are_prob_equivalent ;
s,u -are_prob_equivalent by A2, A4, Th6;
hence x in Finseq-EQclass s by A3; :: thesis: verum

end;

then A5: Finseq-EQclass t c= Finseq-EQclass s by TARSKI:def 3;

now

let x be set ; :: thesis: ( x in Finseq-EQclass s implies x in Finseq-EQclass t )
assume x in Finseq-EQclass s ; :: thesis: x in Finseq-EQclass t
then consider u being FinSequence of S such that
A6: x = u and
A7: s,u -are_prob_equivalent ;
t,u -are_prob_equivalent by A2, A7, Th6;
hence x in Finseq-EQclass t by A6; :: thesis: verum

end;

then Finseq-EQclass s c= Finseq-EQclass t by TARSKI:def 3;
hence Finseq-EQclass t = Finseq-EQclass s by A5, XBOOLE_0:def 10; :: thesis: verum

end;

now

assume Finseq-EQclass s = Finseq-EQclass t ; :: thesis: s,t -are_prob_equivalent
then s in Finseq-EQclass t ;
hence s,t -are_prob_equivalent by Th7; :: thesis: verum

end;

hence ( s,t -are_prob_equivalent iff Finseq-EQclass s = Finseq-EQclass t ) by A1; :: thesis: verum