set X = V;
let s1, s2 be SortSymbol of S; :: thesis: ( t in FreeSort V,s1 & t in FreeSort V,s2 implies s1 = s2 )
assume that
A1: t in FreeSort V,s1 and
A2: t in FreeSort V,s2 ; :: thesis: s1 = s2
FreeSort V,s1 = { a where a is Element of TS (DTConMSA V) : ( ex x being set st
( x in V . s1 & a = root-tree [x,s1] ) or ex o being OperSymbol of S st
( [o,the carrier of S] = a . {} & the_result_sort_of o = s1 ) ) } by MSAFREE:def 12;
then consider a1 being Element of TS (DTConMSA V) such that
A3: t = a1 and
A4: ( ex x being set st
( x in V . s1 & a1 = root-tree [x,s1] ) or ex o being OperSymbol of S st
( [o,the carrier of S] = a1 . {} & the_result_sort_of o = s1 ) ) by A1;
FreeSort V,s2 = { a where a is Element of TS (DTConMSA V) : ( ex x being set st
( x in V . s2 & a = root-tree [x,s2] ) or ex o being OperSymbol of S st
( [o,the carrier of S] = a . {} & the_result_sort_of o = s2 ) ) } by MSAFREE:def 12;
then consider a2 being Element of TS (DTConMSA V) such that
A5: t = a2 and
A6: ( ex x being set st
( x in V . s2 & a2 = root-tree [x,s2] ) or ex o being OperSymbol of S st
( [o,the carrier of S] = a2 . {} & the_result_sort_of o = s2 ) ) by A2;

per cases ( ex x being set st
( x in V . s1 & a1 = root-tree [x,s1] ) or ex o being OperSymbol of S st
( [o,the carrier of S] = a1 . {} & the_result_sort_of o = s1 ) ) by A4;

suppose ex x being set st
( x in V . s1 & a1 = root-tree [x,s1] ) ; :: thesis: s1 = s2

then consider x1 being set such that
A7: ( x1 in V . s1 & a1 = root-tree [x1,s1] ) ;
A8: ( t . {} = [x1,s1] & [x1,s1] `2 = s1 ) by A3, A7, MCART_1:7, TREES_4:3;

now

let o be OperSymbol of S; :: thesis: not [o,the carrier of S] = [x1,s1]
assume [o,the carrier of S] = [x1,s1] ; :: thesis: contradiction
then the carrier of S = s1 by ZFMISC_1:33;
hence contradiction by Lm7; :: thesis: verum

end;

then consider x2 being set such that
A9: ( x2 in V . s2 & a2 = root-tree [x2,s2] ) by A5, A6, A8;
[x1,s1] = [x2,s2] by A3, A5, A7, A9, TREES_4:4;
hence s1 = s2 by ZFMISC_1:33; :: thesis: verum

end;

suppose ex o being OperSymbol of S st
( [o,the carrier of S] = a1 . {} & the_result_sort_of o = s1 ) ; :: thesis: s1 = s2

then consider o1 being OperSymbol of S such that
A10: ( [o1,the carrier of S] = a1 . {} & the_result_sort_of o1 = s1 ) ;

now

given x2 being set such that A11: ( x2 in V . s2 & a2 = root-tree [x2,s2] ) ; :: thesis: contradiction
[o1,the carrier of S] = [x2,s2] by A3, A5, A10, A11, TREES_4:3;
then the carrier of S = s2 by ZFMISC_1:33;
hence contradiction by Lm7; :: thesis: verum

end;

then consider o being OperSymbol of S such that
A12: ( [o,the carrier of S] = t . {} & the_result_sort_of o = s2 ) by A5, A6;
thus s1 = s2 by A3, A10, A12, ZFMISC_1:33; :: thesis: verum

end;

end;