let S be non empty non void ManySortedSign ; :: thesis: for X being V5() ManySortedSet of the carrier of S
for s1, s2 being SortSymbol of S st s1 <> s2 holds
(FreeSort X) . s1 misses (FreeSort X) . s2
let X be V5() ManySortedSet of the carrier of S; :: thesis: for s1, s2 being SortSymbol of S st s1 <> s2 holds
(FreeSort X) . s1 misses (FreeSort X) . s2
let s1, s2 be SortSymbol of S; :: thesis: ( s1 <> s2 implies (FreeSort X) . s1 misses (FreeSort X) . s2 )
assume that
A1: s1 <> s2 and
A2: ((FreeSort X) . s1) /\ ((FreeSort X) . s2) <> {} ; :: according to XBOOLE_0:def 7 :: thesis: contradiction
consider x being set such that
A3: x in ((FreeSort X) . s1) /\ ((FreeSort X) . s2) by A2, XBOOLE_0:def 1;
set D = DTConMSA X;
A4: (FreeSort X) . s1 = FreeSort X,s1 by Def13;
A5: (FreeSort X) . s2 = FreeSort X,s2 by Def13;
x in (FreeSort X) . s2 by A3, XBOOLE_0:def 4;
then consider b being Element of TS (DTConMSA X) such that
A6: b = x and
A7: ( ex x2 being set st
( x2 in X . s2 & b = root-tree [x2,s2] ) or ex o2 being OperSymbol of S st
( [o2,the carrier of S] = b . {} & the_result_sort_of o2 = s2 ) ) by A5;
x in (FreeSort X) . s1 by A3, XBOOLE_0:def 4;
then consider a being Element of TS (DTConMSA X) such that
A8: a = x and
A9: ( ex x1 being set st
( x1 in X . s1 & a = root-tree [x1,s1] ) or ex o1 being OperSymbol of S st
( [o1,the carrier of S] = a . {} & the_result_sort_of o1 = s1 ) ) by A4;

per cases ( ex x1 being set st
( x1 in X . s1 & a = root-tree [x1,s1] ) or ex o1 being OperSymbol of S st
( [o1,the carrier of S] = a . {} & the_result_sort_of o1 = s1 ) ) by A9;

suppose ex x1 being set st
( x1 in X . s1 & a = root-tree [x1,s1] ) ; :: thesis: contradiction

then consider x1 being set such that
x1 in X . s1 and
A10: a = root-tree [x1,s1] ;

now

per cases ( ex x2 being set st
( x2 in X . s2 & b = root-tree [x2,s2] ) or ex o2 being OperSymbol of S st
( [o2,the carrier of S] = b . {} & the_result_sort_of o2 = s2 ) ) by A7;

case ex x2 being set st
( x2 in X . s2 & b = root-tree [x2,s2] ) ; :: thesis: contradiction

then consider x2 being set such that
x2 in X . s2 and
A11: b = root-tree [x2,s2] ;
[x1,s1] = [x2,s2] by A8, A6, A10, A11, TREES_4:4;
hence contradiction by A1, ZFMISC_1:33; :: thesis: verum

end;

case ex o2 being OperSymbol of S st
( [o2,the carrier of S] = b . {} & the_result_sort_of o2 = s2 ) ; :: thesis: contradiction

then consider o2 being OperSymbol of S such that
A12: [o2,the carrier of S] = b . {} and
the_result_sort_of o2 = s2 ;
[o2,the carrier of S] = [x1,s1] by A8, A6, A10, A12, TREES_4:3;
then A13: the carrier of S = s1 by ZFMISC_1:33;
for X being set holds not X in X ;
hence contradiction by A13; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

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

then consider o1 being OperSymbol of S such that
A14: [o1,the carrier of S] = a . {} and
A15: the_result_sort_of o1 = s1 ;

now

per cases ( ex x2 being set st
( x2 in X . s2 & b = root-tree [x2,s2] ) or ex o2 being OperSymbol of S st
( [o2,the carrier of S] = b . {} & the_result_sort_of o2 = s2 ) ) by A7;

case ex x2 being set st
( x2 in X . s2 & b = root-tree [x2,s2] ) ; :: thesis: contradiction

then consider x2 being set such that
x2 in X . s2 and
A16: b = root-tree [x2,s2] ;
[o1,the carrier of S] = [x2,s2] by A8, A6, A14, A16, TREES_4:3;
then A17: the carrier of S = s2 by ZFMISC_1:33;
for X being set holds not X in X ;
hence contradiction by A17; :: thesis: verum

end;

case ex o2 being OperSymbol of S st
( [o2,the carrier of S] = b . {} & the_result_sort_of o2 = s2 ) ; :: thesis: contradiction

hence contradiction by A1, A8, A6, A14, A15, ZFMISC_1:33; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

end;