let S be non empty non void ManySortedSign ; :: thesis: for X being non-empty ManySortedSet of the carrier of S
for t being Element of (Free (S,X))
for xi1, xi2 being FinSequence st xi1 <> xi2 & xi1 in dom t & xi2 in dom t holds
for s1, s2 being SortSymbol of S
for x1 being Element of X . s1
for x2 being Element of X . s2 st t . xi1 = [x1,s1] holds
not xi1 is_a_prefix_of xi2
let X be non-empty ManySortedSet of the carrier of S; :: thesis: for t being Element of (Free (S,X))
for xi1, xi2 being FinSequence st xi1 <> xi2 & xi1 in dom t & xi2 in dom t holds
for s1, s2 being SortSymbol of S
for x1 being Element of X . s1
for x2 being Element of X . s2 st t . xi1 = [x1,s1] holds
not xi1 is_a_prefix_of xi2
let t be Element of (Free (S,X)); :: thesis: for xi1, xi2 being FinSequence st xi1 <> xi2 & xi1 in dom t & xi2 in dom t holds
for s1, s2 being SortSymbol of S
for x1 being Element of X . s1
for x2 being Element of X . s2 st t . xi1 = [x1,s1] holds
not xi1 is_a_prefix_of xi2
let xi1, xi2 be FinSequence; :: thesis: ( xi1 <> xi2 & xi1 in dom t & xi2 in dom t implies for s1, s2 being SortSymbol of S
for x1 being Element of X . s1
for x2 being Element of X . s2 st t . xi1 = [x1,s1] holds
not xi1 is_a_prefix_of xi2 )
assume Z0: xi1 <> xi2 ; :: thesis: ( not xi1 in dom t or not xi2 in dom t or for s1, s2 being SortSymbol of S
for x1 being Element of X . s1
for x2 being Element of X . s2 st t . xi1 = [x1,s1] holds
not xi1 is_a_prefix_of xi2 )
assume xi1 in dom t ; :: thesis: ( not xi2 in dom t or for s1, s2 being SortSymbol of S
for x1 being Element of X . s1
for x2 being Element of X . s2 st t . xi1 = [x1,s1] holds
not xi1 is_a_prefix_of xi2 )
then reconsider nu1 = xi1 as Element of dom t ;
assume Z2: xi2 in dom t ; :: thesis: for s1, s2 being SortSymbol of S
for x1 being Element of X . s1
for x2 being Element of X . s2 st t . xi1 = [x1,s1] holds
not xi1 is_a_prefix_of xi2
let s1, s2 be SortSymbol of S; :: thesis: for x1 being Element of X . s1
for x2 being Element of X . s2 st t . xi1 = [x1,s1] holds
not xi1 is_a_prefix_of xi2
let x1 be Element of X . s1; :: thesis: for x2 being Element of X . s2 st t . xi1 = [x1,s1] holds
not xi1 is_a_prefix_of xi2
let x2 be Element of X . s2; :: thesis: ( t . xi1 = [x1,s1] implies not xi1 is_a_prefix_of xi2 )
assume Z3: t . xi1 = [x1,s1] ; :: thesis: not xi1 is_a_prefix_of xi2
assume xi1 is_a_prefix_of xi2 ; :: thesis: contradiction
then consider r being FinSequence such that
A1: xi2 = xi1 ^ r by TREES_1:1;
reconsider t1 = t | nu1 as Element of (Free (S,X)) by MSAFREE4:44;
<*> NAT in (dom t) | nu1 by TREES_1:22;
then A2: t1 . {} = t . (nu1 ^ {}) by TREES_2:def 10;
xi2 is Element of dom t by Z2;
then reconsider r = r as FinSequence of NAT by A1, FINSEQ_1:36;

per cases ( ex s being SortSymbol of S ex x being Element of X . s st t1 = x -term or ex o being OperSymbol of S ex p being Element of Args (o,(Free (S,X))) st t1 = o -term p ) by Th16;

suppose ex s being SortSymbol of S ex x being Element of X . s st t1 = x -term ; :: thesis: contradiction

then consider s being SortSymbol of S, x being Element of X . s such that
A4: t1 = x -term ;
dom t1 = (dom t) | nu1 by TREES_2:def 10;
then r in dom t1 by Z2, A1, TREES_1:def 6;
then r in {{}} by A4, TREES_1:29;
then r = {} ;
hence contradiction by Z0, A1; :: thesis: verum

end;

suppose ex o being OperSymbol of S ex p being Element of Args (o,(Free (S,X))) st t1 = o -term p ; :: thesis: contradiction

then consider o being OperSymbol of S, p being Element of Args (o,(Free (S,X))) such that
A3: t1 = o -term p ;
t1 . {} = [o, the carrier of S] by A3, TREES_4:def 4;
then ( s1 in the carrier of S & the carrier of S = s1 ) by A2, Z3, XTUPLE_0:1;
hence contradiction ; :: thesis: verum

end;

end;