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

len p = len (the_arity_of o)

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

len p = len (the_arity_of o)

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

len p = len (the_arity_of o)

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 len p = len (the_arity_of o) )

set s = the_result_sort_of o;

assume A1: [o, the carrier of S] -tree p in the Sorts of (FreeMSA X) . (the_result_sort_of o) ; :: thesis: len p = len (the_arity_of o)

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

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

then A2: [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;

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;

reconsider O = [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)) as non empty set ;

reconsider R = REL X as Relation of O,(O *) ;

A3: DTConMSA X = DTConstrStr(# O,R #) by MSAFREE:def 8;

then reconsider TSDT = TS (DTConMSA X) as Subset of (FinTrees O) ;

reconsider c = nt as Element of O by A3;

for x being object st x in TSDT holds

x is DecoratedTree of O ;

then reconsider TSDT = TSDT as DTree-set of O by TREES_3:def 6;

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

A4: 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 ) ) by A2;

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

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

A5: a = nt -tree ts and

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

reconsider ts9 = ts as FinSequence of TSDT ;

reconsider b = roots ts9 as FinSequence of O ;

reconsider b = b as Element of O * by FINSEQ_1:def 11;

[c,b] in R by A6, A3, LANG1:def 1;

then A7: len (roots ts) = len (the_arity_of o) by MSAFREE:def 7;

reconsider ts = ts as DTree-yielding FinSequence ;

A8: dom (roots ts) = dom ts by TREES_3:def 18;

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

hence len p = len (the_arity_of o) by A7, A8, FINSEQ_3:29; :: 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

len p = len (the_arity_of o)

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

len p = len (the_arity_of o)

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

len p = len (the_arity_of o)

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 len p = len (the_arity_of o) )

set s = the_result_sort_of o;

assume A1: [o, the carrier of S] -tree p in the Sorts of (FreeMSA X) . (the_result_sort_of o) ; :: thesis: len p = len (the_arity_of o)

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

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

then A2: [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;

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;

reconsider O = [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)) as non empty set ;

reconsider R = REL X as Relation of O,(O *) ;

A3: DTConMSA X = DTConstrStr(# O,R #) by MSAFREE:def 8;

then reconsider TSDT = TS (DTConMSA X) as Subset of (FinTrees O) ;

reconsider c = nt as Element of O by A3;

for x being object st x in TSDT holds

x is DecoratedTree of O ;

then reconsider TSDT = TSDT as DTree-set of O by TREES_3:def 6;

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

A4: 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 ) ) by A2;

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

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

A5: a = nt -tree ts and

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

reconsider ts9 = ts as FinSequence of TSDT ;

reconsider b = roots ts9 as FinSequence of O ;

reconsider b = b as Element of O * by FINSEQ_1:def 11;

[c,b] in R by A6, A3, LANG1:def 1;

then A7: len (roots ts) = len (the_arity_of o) by MSAFREE:def 7;

reconsider ts = ts as DTree-yielding FinSequence ;

A8: dom (roots ts) = dom ts by TREES_3:def 18;

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

hence len p = len (the_arity_of o) by A7, A8, FINSEQ_3:29; :: thesis: verum