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

assume it1 <> it2 ; :: thesis: contradiction
then not for X being set 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, Th11;
union it2 = the carrier of tfsm by EQREL_1:def 6;
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 Y' = (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:10;
reconsider X = X as Element of it1 by A5;

A12: now

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

proof

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

per cases ( X = Z' or X <> Z' ) ;

suppose X = Z' ; :: thesis: contradiction

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

end;

suppose X <> Z' ; :: thesis: contradiction

then X misses Z' by EQREL_1:def 6;
then X /\ Z' = {} by XBOOLE_0:def 7;
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, Def14; :: thesis: verum

end;

now

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

proof

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

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

suppose Z = Z' ; :: thesis: contradiction

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

end;

suppose Z <> Z' ; :: thesis: contradiction

then Z misses Z' by A8, EQREL_1:def 6;
then Z /\ Z' = {} by XBOOLE_0:def 7;
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, Def14; :: 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, Th11;
union it1 = the carrier of tfsm by EQREL_1:def 6;
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 Y' = (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:10;
reconsider X = X as Element of it2 by A21;

A28: now

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

proof

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

per cases ( X = Z' or X <> Z' ) ;

suppose X = Z' ; :: thesis: contradiction

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

end;

suppose X <> Z' ; :: thesis: contradiction

then X misses Z' by EQREL_1:def 6;
then X /\ Z' = {} by XBOOLE_0:def 7;
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, Def14; :: thesis: verum

end;

now

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

proof

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

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

suppose Z = Z' ; :: thesis: contradiction

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

end;

suppose Z <> Z' ; :: thesis: contradiction

then Z misses Z' by A24, EQREL_1:def 6;
then Z /\ Z' = {} by XBOOLE_0:def 7;
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, Def14; :: thesis: verum

end;

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

end;

end;

end;

hence it1 = it2 ; :: thesis: verum