support (SMoebius X) = X /\ SCNAT by Def5;
hence SMoebius X is finite-support by POLYNOM1:def 8; :: thesis: verum