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;