let it1, it2 be a_partition of the carrier of tfsm; :: thesis: ( it1 is final & it2 is final implies it1 = it2 )
assume that
A2: it1 is final and
A3: it2 is final ; :: thesis: it1 = it2

now :: thesis: not it1 <> it2

assume it1 <> it2 ; :: thesis: contradiction
then not for X being object holds
( X in it1 iff X in it2 ) by TARSKI:2;
then consider X being set such that
A4: ( ( X in it1 & not X in it2 ) or ( not X in it1 & X in it2 ) ) ;

per cases ( ( X in it1 & not X in it2 ) or ( not X in it1 & X in it2 ) ) by A4;

suppose A5: ( X in it1 & not X in it2 ) ; :: thesis: contradiction

then reconsider X = X as Subset of tfsm ;
consider qx being Element of tfsm such that
A6: qx in X by A5, FINSEQ_4:87;
union it2 = the carrier of tfsm by EQREL_1:def 4;
then consider Z being set such that
A7: qx in Z and
A8: Z in it2 by TARSKI:def 4;
reconsider Z = Z as Subset of tfsm by A8;
set XZ = X \ Z;
set ZX = Z \ X;
set Y9 = (X \ Z) \/ (Z \ X);
(X \ Z) \/ (Z \ X) <> {}

proof

assume A9: (X \ Z) \/ (Z \ X) = {} ; :: thesis: contradiction
then Z \ X = {} ;
then A10: Z c= X by XBOOLE_1:37;
X \ Z = {} by A9;
then X c= Z by XBOOLE_1:37;
hence contradiction by A5, A8, A10, XBOOLE_0:def 10; :: thesis: verum

end;

then consider qy being Element of tfsm such that
A11: qy in (X \ Z) \/ (Z \ X) by SUBSET_1:4;
reconsider X = X as Element of it1 by A5;

A12: now :: thesis: not qy in Z \ X

assume A13: qy in Z \ X ; :: thesis: contradiction
A14: not qx,qy -are_equivalent

proof

assume qx,qy -are_equivalent ; :: thesis: contradiction
then consider Z9 being Element of it1 such that
A15: qx in Z9 and
A16: qy in Z9 by A2;

per cases ( X = Z9 or X <> Z9 ) ;

suppose X = Z9 ; :: thesis: contradiction

hence contradiction by A13, A16, XBOOLE_0:def 5; :: thesis: verum

end;

suppose X <> Z9 ; :: thesis: contradiction

then X misses Z9 by EQREL_1:def 4;
then X /\ Z9 = {} ;
hence contradiction by A6, A15, XBOOLE_0:def 4; :: thesis: verum

end;

end;

end;

qy in Z by A13, XBOOLE_0:def 5;
hence contradiction by A3, A7, A8, A14; :: thesis: verum

end;

now :: thesis: not qy in X \ Z

assume A17: qy in X \ Z ; :: thesis: contradiction
A18: not qx,qy -are_equivalent

proof

assume qx,qy -are_equivalent ; :: thesis: contradiction
then consider Z9 being Element of it2 such that
A19: qx in Z9 and
A20: qy in Z9 by A3;

per cases ( Z = Z9 or Z <> Z9 ) ;

suppose Z = Z9 ; :: thesis: contradiction

hence contradiction by A17, A20, XBOOLE_0:def 5; :: thesis: verum

end;

suppose Z <> Z9 ; :: thesis: contradiction

then Z misses Z9 by A8, EQREL_1:def 4;
then Z /\ Z9 = {} ;
hence contradiction by A7, A19, XBOOLE_0:def 4; :: thesis: verum

end;

end;

end;

qy in X by A17, XBOOLE_0:def 5;
hence contradiction by A2, A6, A18; :: thesis: verum

end;

hence contradiction by A11, A12, XBOOLE_0:def 3; :: thesis: verum

end;

suppose A21: ( not X in it1 & X in it2 ) ; :: thesis: contradiction

then reconsider X = X as Subset of tfsm ;
consider qx being Element of tfsm such that
A22: qx in X by A21, FINSEQ_4:87;
union it1 = the carrier of tfsm by EQREL_1:def 4;
then consider Z being set such that
A23: qx in Z and
A24: Z in it1 by TARSKI:def 4;
reconsider Z = Z as Subset of tfsm by A24;
set XZ = X \ Z;
set ZX = Z \ X;
set Y9 = (X \ Z) \/ (Z \ X);
(X \ Z) \/ (Z \ X) <> {}

proof

assume A25: (X \ Z) \/ (Z \ X) = {} ; :: thesis: contradiction
then Z \ X = {} ;
then A26: Z c= X by XBOOLE_1:37;
X \ Z = {} by A25;
then X c= Z by XBOOLE_1:37;
hence contradiction by A21, A24, A26, XBOOLE_0:def 10; :: thesis: verum

end;

then consider qy being Element of tfsm such that
A27: qy in (X \ Z) \/ (Z \ X) by SUBSET_1:4;
reconsider X = X as Element of it2 by A21;

A28: now :: thesis: not qy in Z \ X

assume A29: qy in Z \ X ; :: thesis: contradiction
A30: not qx,qy -are_equivalent

proof

assume qx,qy -are_equivalent ; :: thesis: contradiction
then consider Z9 being Element of it2 such that
A31: qx in Z9 and
A32: qy in Z9 by A3;

per cases ( X = Z9 or X <> Z9 ) ;

suppose X = Z9 ; :: thesis: contradiction

hence contradiction by A29, A32, XBOOLE_0:def 5; :: thesis: verum

end;

suppose X <> Z9 ; :: thesis: contradiction

then X misses Z9 by EQREL_1:def 4;
then X /\ Z9 = {} ;
hence contradiction by A22, A31, XBOOLE_0:def 4; :: thesis: verum

end;

end;

end;

qy in Z by A29, XBOOLE_0:def 5;
hence contradiction by A2, A23, A24, A30; :: thesis: verum

end;

now :: thesis: not qy in X \ Z

assume A33: qy in X \ Z ; :: thesis: contradiction
A34: not qx,qy -are_equivalent

proof

assume qx,qy -are_equivalent ; :: thesis: contradiction
then consider Z9 being Element of it1 such that
A35: qx in Z9 and
A36: qy in Z9 by A2;

per cases ( Z = Z9 or Z <> Z9 ) ;

suppose Z = Z9 ; :: thesis: contradiction

hence contradiction by A33, A36, XBOOLE_0:def 5; :: thesis: verum

end;

suppose Z <> Z9 ; :: thesis: contradiction

then Z misses Z9 by A24, EQREL_1:def 4;
then Z /\ Z9 = {} ;
hence contradiction by A23, A35, XBOOLE_0:def 4; :: thesis: verum

end;

end;

end;

qy in X by A33, XBOOLE_0:def 5;
hence contradiction by A3, A22, A34; :: thesis: verum

end;

hence contradiction by A27, A28, XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

hence it1 = it2 ; :: thesis: verum