reconsider t = t as Term of S,(X (\/) ( the carrier of S --> {0})) by MSAFREE3:8;
(S variables_in t) . s = (variables_in t) . s ;
hence (S variables_in t) . s is finite ; :: thesis: verum