reconsider t = t as Term of the carrier of (DTConMSA (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