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 10;
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 10;
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
x1 in V . s1 and
A7: a1 = root-tree [x1,s1] ;
now :: thesis: for o being OperSymbol of S holds not [o, the carrier of S] = [x1,s1]
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 XTUPLE_0:1;
hence contradiction by Lm7; :: thesis: verum
end;
then consider x2 being set such that
x2 in V . s2 and
A8: a2 = root-tree [x2,s2] by A3, A5, A6, A7, TREES_4:3;
[x1,s1] = [x2,s2] by A3, A5, A7, A8, TREES_4:4;
hence s1 = s2 by XTUPLE_0:1; :: 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
A9: [o1, the carrier of S] = a1 . {} and
A10: the_result_sort_of o1 = s1 ;
now :: thesis: for x2 being set holds
( not x2 in V . s2 or not a2 = root-tree [x2,s2] )
given x2 being set such that x2 in V . s2 and
A11: a2 = root-tree [x2,s2] ; :: thesis: contradiction
[o1, the carrier of S] = [x2,s2] by A3, A5, A9, A11, TREES_4:3;
then the carrier of S = s2 by XTUPLE_0:1;
hence contradiction by Lm7; :: thesis: verum
end;
hence s1 = s2 by A3, A5, A6, A9, A10, XTUPLE_0:1; :: thesis: verum
end;
end;