let g be non zero Polynomial of INT.Ring; :: thesis: rng |.g.| is finite
reconsider g1 = |.g.| as Element of the carrier of (Polynom-Ring INT.Ring) by POLYNOM3:def 10;
A1: rng g1 = (g1 .: (Support g1)) \/ {(0. INT.Ring)} by E_TRANS1:8;
Support g1 is finite by POLYNOM1:def 5;
hence rng |.g.| is finite by A1; :: thesis: verum