let S be non empty non void ManySortedSign ; for X being V5() 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 V5() 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 t be 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 xi1, xi2 be FinSequence; ( 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
; ( 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
; ( 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
; 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; 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; 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; ( t . xi1 = [x1,s1] implies not xi1 is_a_prefix_of xi2 )
assume Z3:
t . xi1 = [x1,s1]
; not xi1 is_a_prefix_of xi2
assume
xi1 is_a_prefix_of xi2
; 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;