set S = the carrier of tfsm;
let IT1, IT2 be Equivalence_Relation of the carrier of tfsm; :: thesis: ( ( for qa, qb being State of tfsm holds
( [qa,qb] in IT1 iff i -equivalent qa,qb ) ) & ( for qa, qb being State of tfsm holds
( [qa,qb] in IT2 iff i -equivalent qa,qb ) ) implies IT1 = IT2 )
assume A5: for qa, qb being Element of the carrier of tfsm holds
( [qa,qb] in IT1 iff i -equivalent qa,qb ) ; :: thesis: ( ex qa, qb being State of tfsm st
( ( [qa,qb] in IT2 implies i -equivalent qa,qb ) implies ( i -equivalent qa,qb & not [qa,qb] in IT2 ) ) or IT1 = IT2 )
assume A6: for qa, qb being Element of the carrier of tfsm holds
( [qa,qb] in IT2 iff i -equivalent qa,qb ) ; :: thesis: IT1 = IT2
assume IT1 <> IT2 ; :: thesis: contradiction
then consider x being object such that
A7: ( ( x in IT1 & not x in IT2 ) or ( x in IT2 & not x in IT1 ) ) by TARSKI:2;

per cases ( ( x in IT1 & not x in IT2 ) or ( x in IT2 & not x in IT1 ) ) by A7;

suppose A8: ( x in IT1 & not x in IT2 ) ; :: thesis: contradiction

then consider qa, qb being object such that
A9: x = [qa,qb] and
A10: ( qa in the carrier of tfsm & qb in the carrier of tfsm ) by RELSET_1:2;
reconsider qa = qa, qb = qb as Element of the carrier of tfsm by A10;
i -equivalent qa,qb by A5, A8, A9;
hence contradiction by A6, A8, A9; :: thesis: verum

end;

suppose A11: ( x in IT2 & not x in IT1 ) ; :: thesis: contradiction

then consider qa, qb being object such that
A12: x = [qa,qb] and
A13: ( qa in the carrier of tfsm & qb in the carrier of tfsm ) by RELSET_1:2;
reconsider qa = qa, qb = qb as Element of the carrier of tfsm by A13;
i -equivalent qa,qb by A6, A11, A12;
hence contradiction by A5, A11, A12; :: thesis: verum

end;

end;