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 A6: 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 A7: 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 set such that
A8: ( ( 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 A8;

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

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

end;

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

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

end;

end;