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 () . holds
for i being Nat st i in dom () holds
p . i in the Sorts of () . (() . 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 () . holds
for i being Nat st i in dom () holds
p . i in the Sorts of () . (() . 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 () . holds
for i being Nat st i in dom () holds
p . i in the Sorts of () . (() . i)

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

A1: FreeMSA X = MSAlgebra(# (),() #) by MSAFREE:def 14;
assume A2: [o, the carrier of S] -tree p in the Sorts of () . ; :: thesis: for i being Nat st i in dom () holds
p . i in the Sorts of () . (() . i)

now :: thesis: for i being Nat st i in dom () holds
p . i in the Sorts of () . (() . 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 () 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 () implies p . i in the Sorts of () . (() . i) )
assume A3: i in dom () ; :: thesis: p . i in the Sorts of () . (() . 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 () . s = FreeSort (X,s) by
.= FreeSort (X,(() /. i)) by ;
[o, the carrier of S] -tree p in FreeSort (X,) by ;
then [o, the carrier of S] -tree p in { a where a is Element of TS () : ( ex x being set st
( x in X . & a = root-tree [x,] ) 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 () such that
A5: a = [o, the carrier of S] -tree p and
( ex x being set st
( x in X . & a = root-tree [x,] ) 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 ;
then consider ts being FinSequence of TS () 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 ((() #) * the Arity of S) . o by ;
( dom p = Seg (len p) & dom () = Seg (len ()) ) 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 ;
hence p . i in the Sorts of () . (() . i) by ; :: thesis: verum
end;
hence for i being Nat st i in dom () holds
p . i in the Sorts of () . (() . i) ; :: thesis: verum