for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of S
for w being ManySortedFunction of X, the carrier of S --> NAT
for o being OperSymbol of S
for p being ArgumentSeq of Sym (o,X)
for q being FinSequence st dom q = dom p & ( for i being Nat
for t being Element of (Free (S,X)) st i in dom p & t = p . i holds
q . i = # (t,w) ) holds
# (((Sym (o,X)) -tree p),w) = (Sym (o,( the carrier of S --> NAT))) -tree q