let S be non empty non void ManySortedSign ; :: thesis: for X being V5() ManySortedSet of the carrier of S
for v being Vertex of S
for o being OperSymbol of S
for e being Element of the Sorts of () . v st e . {} = [o, the carrier of S] holds
ex p being DTree-yielding FinSequence st
( len p = len () & ( for i being Nat st i in dom p holds
p . i in the Sorts of () . (() . i) ) )

let X be V5() ManySortedSet of the carrier of S; :: thesis: for v being Vertex of S
for o being OperSymbol of S
for e being Element of the Sorts of () . v st e . {} = [o, the carrier of S] holds
ex p being DTree-yielding FinSequence st
( len p = len () & ( for i being Nat st i in dom p holds
p . i in the Sorts of () . (() . i) ) )

let v be Vertex of S; :: thesis: for o being OperSymbol of S
for e being Element of the Sorts of () . v st e . {} = [o, the carrier of S] holds
ex p being DTree-yielding FinSequence st
( len p = len () & ( for i being Nat st i in dom p holds
p . i in the Sorts of () . (() . i) ) )

let o be OperSymbol of S; :: thesis: for e being Element of the Sorts of () . v st e . {} = [o, the carrier of S] holds
ex p being DTree-yielding FinSequence st
( len p = len () & ( for i being Nat st i in dom p holds
p . i in the Sorts of () . (() . i) ) )

let e be Element of the Sorts of () . v; :: thesis: ( e . {} = [o, the carrier of S] implies ex p being DTree-yielding FinSequence st
( len p = len () & ( for i being Nat st i in dom p holds
p . i in the Sorts of () . (() . i) ) ) )

assume A1: e . {} = [o, the carrier of S] ; :: thesis: ex p being DTree-yielding FinSequence st
( len p = len () & ( for i being Nat st i in dom p 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;
FreeMSA X = MSAlgebra(# (),() #) by MSAFREE:def 14;
then the Sorts of () . v = FreeSort (X,v) by MSAFREE:def 11;
then e in FreeSort (X,v) ;
then e in { a where a is Element of TS () : ( ex x being set st
( x in X . v & a = root-tree [x,v] ) or ex o being OperSymbol of S st
( [o, the carrier of S] = a . {} & the_result_sort_of o = v ) )
}
by MSAFREE:def 10;
then consider a being Element of TS () such that
A2: a = e and
A3: ( ex x being set st
( x in X . v & a = root-tree [x,v] ) or ex o being OperSymbol of S st
( [o, the carrier of S] = a . {} & the_result_sort_of o = v ) ) ;
consider x being set such that
A4: ( ( x in X . v & a = root-tree [x,v] ) or ex o being OperSymbol of S st
( [o, the carrier of S] = a . {} & the_result_sort_of o = v ) ) by A3;
consider p being FinSequence of TS () such that
A5: a = nt -tree p and
nt ==> roots p by ;
now :: thesis: not a = root-tree [x,v]
assume a = root-tree [x,v] ; :: thesis: contradiction
then A6: a . {} = [x,v] by TREES_4:3;
A7: for X being set holds not X in X ;
a . {} = [o, the carrier of S] by ;
then the carrier of S = v by ;
hence contradiction by A7; :: thesis: verum
end;
then consider o9 being OperSymbol of S such that
A8: [o9, the carrier of S] = a . {} and
A9: the_result_sort_of o9 = v by A4;
A10: o = o9 by ;
then A11: len p = len () by A2, A5, A9, Th10;
then dom p = Seg (len ()) by FINSEQ_1:def 3
.= dom () by FINSEQ_1:def 3 ;
then for i being Nat st i in dom p holds
p . i in the Sorts of () . (() . i) by A2, A5, A9, A10, Th11;
hence ex p being DTree-yielding FinSequence st
( len p = len () & ( for i being Nat st i in dom p holds
p . i in the Sorts of () . (() . i) ) ) by A11; :: thesis: verum