let S be non empty non void ManySortedSign ; :: thesis: for X being non-empty 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 (FreeMSA X) . v st e . {} = [o, the carrier of S] holds
ex p being DTree-yielding FinSequence st
( len p = len (the_arity_of o) & ( for i being Nat st i in dom p holds
p . i in the Sorts of (FreeMSA X) . ((the_arity_of o) . i) ) )
let X be non-empty 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 (FreeMSA X) . v st e . {} = [o, the carrier of S] holds
ex p being DTree-yielding FinSequence st
( len p = len (the_arity_of o) & ( for i being Nat st i in dom p holds
p . i in the Sorts of (FreeMSA X) . ((the_arity_of o) . i) ) )
let v be Vertex of S; :: thesis: for o being OperSymbol of S
for e being Element of the Sorts of (FreeMSA X) . v st e . {} = [o, the carrier of S] holds
ex p being DTree-yielding FinSequence st
( len p = len (the_arity_of o) & ( for i being Nat st i in dom p holds
p . i in the Sorts of (FreeMSA X) . ((the_arity_of o) . i) ) )
let o be OperSymbol of S; :: thesis: for e being Element of the Sorts of (FreeMSA X) . v st e . {} = [o, the carrier of S] holds
ex p being DTree-yielding FinSequence st
( len p = len (the_arity_of o) & ( for i being Nat st i in dom p holds
p . i in the Sorts of (FreeMSA X) . ((the_arity_of o) . i) ) )
let e be Element of the Sorts of (FreeMSA X) . v; :: thesis: ( e . {} = [o, the carrier of S] implies ex p being DTree-yielding FinSequence st
( len p = len (the_arity_of o) & ( for i being Nat st i in dom p holds
p . i in the Sorts of (FreeMSA X) . ((the_arity_of o) . i) ) ) )
assume A1: e . {} = [o, the carrier of S] ; :: thesis: ex p being DTree-yielding FinSequence st
( len p = len (the_arity_of o) & ( for i being Nat st i in dom p 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;
FreeMSA X = MSAlgebra(# (FreeSort X),(FreeOper X) #) by MSAFREE:def 14;
then the Sorts of (FreeMSA X) . v = FreeSort (X,v) by MSAFREE:def 11;
then e in FreeSort (X,v) ;
then e in { a where a is Element of TS (DTConMSA X) : ( 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 (DTConMSA X) 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 (DTConMSA X) such that
A5: a = nt -tree p and
nt ==> roots p by A1, A2, DTCONSTR:10;

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 A5, TREES_4:def 4;
then the carrier of S = v by A6, XTUPLE_0:1;
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 A1, A2, A8, XTUPLE_0:1;
then A11: len p = len (the_arity_of o) by A2, A5, A9, Th10;
then dom p = Seg (len (the_arity_of o)) by FINSEQ_1:def 3
.= dom (the_arity_of o) by FINSEQ_1:def 3 ;
then for i being Nat st i in dom p holds
p . i in the Sorts of (FreeMSA X) . ((the_arity_of o) . i) by A2, A5, A9, A10, Th11;
hence ex p being DTree-yielding FinSequence st
( len p = len (the_arity_of o) & ( for i being Nat st i in dom p holds
p . i in the Sorts of (FreeMSA X) . ((the_arity_of o) . i) ) ) by A11; :: thesis: verum