theorem Th93: :: ABCMIZ_1:93

for S being ManySortedSign
for o being set
for t being DecoratedTree holds S variables_in ([o, the carrier of S] -tree <*t*>) = S variables_in t