let S be non empty non void ManySortedSign ; :: thesis: for X being V5() ManySortedSet of the carrier of S

for o being OperSymbol of S

for p being DTree-yielding FinSequence st [o, the carrier of S] -tree p in the Sorts of (FreeMSA X) . (the_result_sort_of o) holds

for i being Nat st i in dom (the_arity_of o) holds

p . i in the Sorts of (FreeMSA X) . ((the_arity_of o) . i)

let X be V5() ManySortedSet of the carrier of S; :: thesis: for o being OperSymbol of S

for p being DTree-yielding FinSequence st [o, the carrier of S] -tree p in the Sorts of (FreeMSA X) . (the_result_sort_of o) holds

for i being Nat st i in dom (the_arity_of o) holds

p . i in the Sorts of (FreeMSA X) . ((the_arity_of o) . i)

let o be OperSymbol of S; :: thesis: for p being DTree-yielding FinSequence st [o, the carrier of S] -tree p in the Sorts of (FreeMSA X) . (the_result_sort_of o) holds

for i being Nat st i in dom (the_arity_of o) holds

p . i in the Sorts of (FreeMSA X) . ((the_arity_of o) . i)

let p be DTree-yielding FinSequence; :: thesis: ( [o, the carrier of S] -tree p in the Sorts of (FreeMSA X) . (the_result_sort_of o) implies for i being Nat st i in dom (the_arity_of o) holds

p . i in the Sorts of (FreeMSA X) . ((the_arity_of o) . i) )

A1: FreeMSA X = MSAlgebra(# (FreeSort X),(FreeOper X) #) by MSAFREE:def 14;

assume A2: [o, the carrier of S] -tree p in the Sorts of (FreeMSA X) . (the_result_sort_of o) ; :: thesis: for i being Nat st i in dom (the_arity_of o) holds

p . i in the Sorts of (FreeMSA X) . ((the_arity_of o) . i)

p . i in the Sorts of (FreeMSA X) . ((the_arity_of o) . i) ; :: thesis: verum

for o being OperSymbol of S

for p being DTree-yielding FinSequence st [o, the carrier of S] -tree p in the Sorts of (FreeMSA X) . (the_result_sort_of o) holds

for i being Nat st i in dom (the_arity_of o) holds

p . i in the Sorts of (FreeMSA X) . ((the_arity_of o) . i)

let X be V5() ManySortedSet of the carrier of S; :: thesis: for o being OperSymbol of S

for p being DTree-yielding FinSequence st [o, the carrier of S] -tree p in the Sorts of (FreeMSA X) . (the_result_sort_of o) holds

for i being Nat st i in dom (the_arity_of o) holds

p . i in the Sorts of (FreeMSA X) . ((the_arity_of o) . i)

let o be OperSymbol of S; :: thesis: for p being DTree-yielding FinSequence st [o, the carrier of S] -tree p in the Sorts of (FreeMSA X) . (the_result_sort_of o) holds

for i being Nat st i in dom (the_arity_of o) holds

p . i in the Sorts of (FreeMSA X) . ((the_arity_of o) . i)

let p be DTree-yielding FinSequence; :: thesis: ( [o, the carrier of S] -tree p in the Sorts of (FreeMSA X) . (the_result_sort_of o) implies for i being Nat st i in dom (the_arity_of o) holds

p . i in the Sorts of (FreeMSA X) . ((the_arity_of o) . i) )

A1: FreeMSA X = MSAlgebra(# (FreeSort X),(FreeOper X) #) by MSAFREE:def 14;

assume A2: [o, the carrier of S] -tree p in the Sorts of (FreeMSA X) . (the_result_sort_of o) ; :: thesis: for i being Nat st i in dom (the_arity_of o) holds

p . i in the Sorts of (FreeMSA X) . ((the_arity_of o) . i)

now :: thesis: for i being Nat st i in dom (the_arity_of o) holds

p . i in the Sorts of (FreeMSA X) . ((the_arity_of o) . i)

hence
for i being Nat st i in dom (the_arity_of o) holds p . i in the Sorts of (FreeMSA X) . ((the_arity_of o) . i)

the carrier of S in { the carrier of S}
by TARSKI:def 1;

then [o, the carrier of S] in [: the carrier' of S,{ the carrier of S}:] by ZFMISC_1:87;

then reconsider nt = [o, the carrier of S] as NonTerminal of (DTConMSA X) by MSAFREE:6;

set rso = the_result_sort_of o;

reconsider ao = the_arity_of o as Element of the carrier of S * ;

let i be Nat; :: thesis: ( i in dom (the_arity_of o) implies p . i in the Sorts of (FreeMSA X) . ((the_arity_of o) . i) )

assume A3: i in dom (the_arity_of o) ; :: thesis: p . i in the Sorts of (FreeMSA X) . ((the_arity_of o) . i)

then ao . i in rng ao by FUNCT_1:def 3;

then reconsider s = ao . i as SortSymbol of S ;

A4: the Sorts of (FreeMSA X) . s = FreeSort (X,s) by A1, MSAFREE:def 11

.= FreeSort (X,((the_arity_of o) /. i)) by A3, PARTFUN1:def 6 ;

[o, the carrier of S] -tree p in FreeSort (X,(the_result_sort_of o)) by A2, A1, MSAFREE:def 11;

then [o, the carrier of S] -tree p in { a where a is Element of TS (DTConMSA X) : ( ex x being set st

( x in X . (the_result_sort_of o) & a = root-tree [x,(the_result_sort_of o)] ) or ex o being OperSymbol of S st

( [o, the carrier of S] = a . {} & the_result_sort_of o = the_result_sort_of o ) ) } by MSAFREE:def 10;

then consider a being Element of TS (DTConMSA X) such that

A5: a = [o, the carrier of S] -tree p and

( ex x being set st

( x in X . (the_result_sort_of o) & a = root-tree [x,(the_result_sort_of o)] ) or ex o being OperSymbol of S st

( [o, the carrier of S] = a . {} & the_result_sort_of o = the_result_sort_of o ) ) ;

a . {} = [o, the carrier of S] by A5, TREES_4:def 4;

then consider ts being FinSequence of TS (DTConMSA X) such that

A6: a = nt -tree ts and

A7: nt ==> roots ts by DTCONSTR:10;

nt = Sym (o,X) by MSAFREE:def 9;

then A8: ts in (((FreeSort X) #) * the Arity of S) . o by A7, MSAFREE:10;

( dom p = Seg (len p) & dom (the_arity_of o) = Seg (len (the_arity_of o)) ) by FINSEQ_1:def 3;

then A9: i in dom p by A2, A3, Th10;

reconsider ts = ts as DTree-yielding FinSequence ;

ts = p by A5, A6, TREES_4:15;

hence p . i in the Sorts of (FreeMSA X) . ((the_arity_of o) . i) by A9, A8, A4, MSAFREE:9; :: thesis: verum

end;then [o, the carrier of S] in [: the carrier' of S,{ the carrier of S}:] by ZFMISC_1:87;

then reconsider nt = [o, the carrier of S] as NonTerminal of (DTConMSA X) by MSAFREE:6;

set rso = the_result_sort_of o;

reconsider ao = the_arity_of o as Element of the carrier of S * ;

let i be Nat; :: thesis: ( i in dom (the_arity_of o) implies p . i in the Sorts of (FreeMSA X) . ((the_arity_of o) . i) )

assume A3: i in dom (the_arity_of o) ; :: thesis: p . i in the Sorts of (FreeMSA X) . ((the_arity_of o) . i)

then ao . i in rng ao by FUNCT_1:def 3;

then reconsider s = ao . i as SortSymbol of S ;

A4: the Sorts of (FreeMSA X) . s = FreeSort (X,s) by A1, MSAFREE:def 11

.= FreeSort (X,((the_arity_of o) /. i)) by A3, PARTFUN1:def 6 ;

[o, the carrier of S] -tree p in FreeSort (X,(the_result_sort_of o)) by A2, A1, MSAFREE:def 11;

then [o, the carrier of S] -tree p in { a where a is Element of TS (DTConMSA X) : ( ex x being set st

( x in X . (the_result_sort_of o) & a = root-tree [x,(the_result_sort_of o)] ) or ex o being OperSymbol of S st

( [o, the carrier of S] = a . {} & the_result_sort_of o = the_result_sort_of o ) ) } by MSAFREE:def 10;

then consider a being Element of TS (DTConMSA X) such that

A5: a = [o, the carrier of S] -tree p and

( ex x being set st

( x in X . (the_result_sort_of o) & a = root-tree [x,(the_result_sort_of o)] ) or ex o being OperSymbol of S st

( [o, the carrier of S] = a . {} & the_result_sort_of o = the_result_sort_of o ) ) ;

a . {} = [o, the carrier of S] by A5, TREES_4:def 4;

then consider ts being FinSequence of TS (DTConMSA X) such that

A6: a = nt -tree ts and

A7: nt ==> roots ts by DTCONSTR:10;

nt = Sym (o,X) by MSAFREE:def 9;

then A8: ts in (((FreeSort X) #) * the Arity of S) . o by A7, MSAFREE:10;

( dom p = Seg (len p) & dom (the_arity_of o) = Seg (len (the_arity_of o)) ) by FINSEQ_1:def 3;

then A9: i in dom p by A2, A3, Th10;

reconsider ts = ts as DTree-yielding FinSequence ;

ts = p by A5, A6, TREES_4:15;

hence p . i in the Sorts of (FreeMSA X) . ((the_arity_of o) . i) by A9, A8, A4, MSAFREE:9; :: thesis: verum

p . i in the Sorts of (FreeMSA X) . ((the_arity_of o) . i) ; :: thesis: verum