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

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

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

let p be DTree-yielding FinSequence; :: thesis: ( [o, the carrier of S] -tree p in the Sorts of () . implies len p = len () )
set s = the_result_sort_of o;
assume A1: [o, the carrier of S] -tree p in the Sorts of () . ; :: thesis: len p = len ()
FreeMSA X = MSAlgebra(# (),() #) by MSAFREE:def 14;
then [o, the carrier of S] -tree p in FreeSort (X,) by ;
then A2: [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;
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;
reconsider O = [: the carrier' of S,{ the carrier of S}:] \/ (Union ()) 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 () as Subset of () ;
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 () such that
A4: 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 ) ) by A2;
a . {} = [o, the carrier of S] by ;
then consider ts being FinSequence of TS () 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 ;
then A7: len (roots ts) = len () 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 ;
hence len p = len () by ; :: thesis: verum