per cases ( a = 0 or a <> 0 ) ;

suppose A1: a = 0 ; :: thesis: a * b is finite-support

thus support (a * b) is finite by A1; :: according to POLYNOM1: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 POLYNOM1:def 8 :: thesis: verum

end;

end;