let g be non zero Polynomial of INT.Ring; :: thesis: ex M being Nat st
for i being Nat holds |.(g . i).| <= M
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;
rng |.g.| c= NAT

proof

let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in rng |.g.| or o in NAT )
assume o in rng |.g.| ; :: thesis: o in NAT
then consider x being object such that
A3: ( x in dom |.g.| & |.g.| . x = o ) by FUNCT_1:def 3;
|.g.| . x = |.(g . x).| by A3, Def9;
hence o in NAT by A3; :: thesis: verum

end;

then reconsider S = rng |.g.| as non empty natural-membered finite set by A1;
max S in S by XXREAL_2:def 8;
then reconsider M = max S as Nat ;
take M ; :: thesis: for i being Nat holds |.(g . i).| <= M
A5: dom |.g.| = NAT by FUNCT_2:def 1;
for i being Nat holds |.(g . i).| <= M

proof

let i be Nat; :: thesis: |.(g . i).| <= M
|.g.| . i = |.(g . i).| by Def9;
then |.(g . i).| in S by A5, ORDINAL1:def 12, FUNCT_1:3;
hence |.(g . i).| <= M by XXREAL_2:def 8; :: thesis: verum

end;

hence for i being Nat holds |.(g . i).| <= M ; :: thesis: verum