set M = Coeff p;
set X = Support p;

now :: thesis: for o being object st o in Coeff p holds
o in p .: (Support p)

let o be object ; :: thesis: ( o in Coeff p implies o in p .: (Support p) )
assume o in Coeff p ; :: thesis: o in p .: (Support p)
then consider i being Element of NAT such that
H1: ( o = p . i & p . i <> 0. F ) ;
H2: dom p = NAT by FUNCT_2:def 1;
then i in Support p by H1, POLYNOM1:def 3;
hence o in p .: (Support p) by H1, H2, FUNCT_1:def 6; :: thesis: verum

end;

then A: Coeff p c= p .: (Support p) ;
Support p is finite by POLYNOM1:def 5;
hence Coeff p is finite by A; :: thesis: verum