let n be set ; :: thesis: for p being finite-Support sequence of INT.Ring holds Support p = Support |.p.|
let p be finite-Support sequence of INT.Ring; :: thesis: Support p = Support |.p.|
A1: ( dom p = NAT & NAT = dom |.p.| ) by FUNCT_2:def 1;
thus Support p c= Support |.p.| :: according to XBOOLE_0:def 10 :: thesis: Support |.p.| c= Support p

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Support p or x in Support |.p.| )
assume x in Support p ; :: thesis: x in Support |.p.|
then ( x in dom p & p . x <> 0. INT.Ring & |.(p . x).| = |.p.| . x ) by Def9, POLYNOM1:def 3;
hence x in Support |.p.| by A1, POLYNOM1:def 3; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Support |.p.| or x in Support p )
assume x in Support |.p.| ; :: thesis: x in Support p
then ( x in dom |.p.| & |.p.| . x <> 0. INT.Ring & |.(p . x).| = |.p.| . x ) by Def9, POLYNOM1:def 3;
then ( x in dom p & p . x <> 0. INT.Ring ) by A1;
hence x in Support p by POLYNOM1:def 3; :: thesis: verum