theorem Th57: :: MSAFREE4:57

for S being non empty non void ManySortedSign
for X being non-empty ManySortedSet of S
for w being ManySortedFunction of X, the carrier of S --> NAT
for s being SortSymbol of S
for x being Element of X . s holds # ((root-tree [x,s]),w) = root-tree [((w . s) . x),s]