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

hereby :: thesis: ( Finseq-EQclass t = Finseq-EQclass s implies t,s -are_prob_equivalent )

assume A1: t,s -are_prob_equivalent ; :: thesis: Finseq-EQclass t = Finseq-EQclass s
thus Finseq-EQclass t = Finseq-EQclass s :: thesis: verum

proof

thus Finseq-EQclass t c= Finseq-EQclass s :: according to XBOOLE_0:def 10 :: thesis: Finseq-EQclass s c= Finseq-EQclass t

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Finseq-EQclass t or 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
A2: x = u and
A3: t,u -are_prob_equivalent ;
s,u -are_prob_equivalent by A1, A3, Th4;
hence x in Finseq-EQclass s by A2; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Finseq-EQclass s or 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
A4: x = u and
A5: s,u -are_prob_equivalent ;
t,u -are_prob_equivalent by A1, A5, Th4;
hence x in Finseq-EQclass t by A4; :: thesis: verum

end;

end;

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