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
() . s1 misses () . s2

let X be V5() ManySortedSet of the carrier of S; :: thesis: for s1, s2 being SortSymbol of S st s1 <> s2 holds
() . s1 misses () . s2

let s1, s2 be SortSymbol of S; :: thesis: ( s1 <> s2 implies () . s1 misses () . s2 )
assume that
A1: s1 <> s2 and
A2: ((FreeSort X) . s1) /\ (() . s2) <> {} ; :: according to XBOOLE_0:def 7 :: thesis: contradiction
consider x being object such that
A3: x in (() . s1) /\ (() . s2) by ;
set D = DTConMSA X;
A4: (FreeSort X) . s1 = FreeSort (X,s1) by Def11;
A5: (FreeSort X) . s2 = FreeSort (X,s2) by Def11;
x in () . s2 by ;
then consider b being Element of TS () 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 () . s1 by ;
then consider a being Element of TS () 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 :: thesis: ( ( ex x2 being set st
( x2 in X . s2 & b = root-tree [x2,s2] ) & contradiction ) or ( ex o2 being OperSymbol of S st
( [o2, the carrier of S] = b . {} & the_result_sort_of o2 = s2 ) & contradiction ) )
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 ;
hence contradiction by A1, XTUPLE_0:1; :: 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 ;
then A13: the carrier of S = s1 by XTUPLE_0:1;
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 :: thesis: ( ( ex x2 being set st
( x2 in X . s2 & b = root-tree [x2,s2] ) & contradiction ) or ( ex o2 being OperSymbol of S st
( [o2, the carrier of S] = b . {} & the_result_sort_of o2 = s2 ) & contradiction ) )
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 ;
then A17: the carrier of S = s2 by XTUPLE_0:1;
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
end;
end;
end;
hence contradiction ; :: thesis: verum
end;
end;