for S being non empty non void ManySortedSign
for X being V2() ManySortedSet of the carrier of S
for v, vk being SortSymbol of S
for o being OperSymbol of S
for t being Element of the Sorts of (FreeMSA X) . v
for a being ArgumentSeq of Sym (o,X)
for k being Element of NAT
for ak being Element of the Sorts of (FreeMSA X) . vk st t = [o, the carrier of S] -tree a & k in dom a & ak = a . k holds
depth ak < depth t