let S be non empty non void ManySortedSign ; :: thesis: for X being V5() ManySortedSet of
for s1, s2 being SortSymbol of S st s1 <> s2 holds
(FreeSort X) . s1 misses (FreeSort X) . s2
let X be V5() ManySortedSet of ; :: 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;
A4: ( x in (FreeSort X) . s1 & x in (FreeSort X) . s2 ) by A3, XBOOLE_0:def 4;
A5: ( (FreeSort X) . s1 = FreeSort X,s1 & (FreeSort X) . s2 = FreeSort X,s2 ) by Def13;
set D = DTConMSA X;
consider a being Element of TS (DTConMSA X) such that
A6: a = x and
A7: ( 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, A5;
consider b being Element of TS (DTConMSA X) such that
A8: b = x and
A9: ( 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 A4, A5;

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 A7;

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

then consider x1 being set such that
A10: ( x1 in X . s1 & 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 A9;

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

then consider x2 being set such that
A11: ( x2 in X . s2 & b = root-tree [x2,s2] ) ;
[x1,s1] = [x2,s2] by A6, A8, 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 . {} & the_result_sort_of o2 = s2 ) ;
[o2,the carrier of S] = [x1,s1] by A6, A8, 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 . {} & 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 A9;

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

then consider x2 being set such that
A15: ( x2 in X . s2 & b = root-tree [x2,s2] ) ;
[o1,the carrier of S] = [x2,s2] by A6, A8, A14, A15, TREES_4:3;
then A16: the carrier of S = s2 by ZFMISC_1:33;
for X being set holds not X in X ;
hence contradiction by A16; :: 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
A17: ( [o2,the carrier of S] = b . {} & the_result_sort_of o2 = s2 ) ;
thus contradiction by A1, A6, A8, A14, A17, ZFMISC_1:33; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

end;