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