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 object 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 Def11;

A5: (FreeSort X) . s2 = FreeSort (X,s2) by Def11;

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;

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 object 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 Def11;

A5: (FreeSort X) . s2 = FreeSort (X,s2) by Def11;

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;

end;

( 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

( 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] ;

end;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 ) )end;

hence
contradiction
; :: thesis: verum( 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;

end;

( 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

( 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, XTUPLE_0:1; :: thesis: verum

end;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, XTUPLE_0:1; :: thesis: verum

case
ex o2 being OperSymbol of S st

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

( [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 XTUPLE_0:1;

for X being set holds not X in X ;

hence contradiction by A13; :: thesis: verum

end;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 XTUPLE_0:1;

for X being set holds not X in X ;

hence contradiction by A13; :: thesis: verum

suppose
ex o1 being OperSymbol of S st

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

( [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 ;

end;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 ) )end;

hence
contradiction
; :: thesis: verum( 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;

end;

( 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

( 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 XTUPLE_0:1;

for X being set holds not X in X ;

hence contradiction by A17; :: thesis: verum

end;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 XTUPLE_0:1;

for X being set holds not X in X ;

hence contradiction by A17; :: thesis: verum

case
ex o2 being OperSymbol of S st

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

end;

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

end;