set Sp = Support p;
set Sq = Support q;
( Support p is finite & Support q is finite ) by Def4;
then (Support p) \/ (Support q) is finite ;
then Support (p + q) is finite by Th20, FINSET_1:1;
hence p + q is finite-Support by Def4; :: thesis: verum