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 (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 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 (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;

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

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 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 (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]

then consider o9 being OperSymbol of S such that 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 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

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