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