per cases ( a = 0 or a <> 0 ) ;
suppose a = 0 ; :: thesis: a * b is finite-support
hence support (a * b) is finite ; :: according to PRE_POLY:def 8 :: thesis: verum
end;
suppose a <> 0 ; :: thesis: a * b is finite-support
then support (a * b) = support b by Th16;
hence support (a * b) is finite ; :: according to PRE_POLY:def 8 :: thesis: verum
end;
end;