let n be set ; :: thesis: for p being Series of n,F_Real holds Support p = Support |.p.|

let p be Series of n,F_Real; :: thesis: Support p = Support |.p.|

A1: ( dom p = Bags n & Bags n = 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

assume x in Support |.p.| ; :: thesis: x in Support p

then ( x in dom |.p.| & |.p.| . x <> 0. F_Real & |.(p . x).| = |.p.| . x ) by Def1, POLYNOM1:def 3;

then ( x in dom p & p . x <> 0. F_Real ) by A1;

hence x in Support p by POLYNOM1:def 3; :: thesis: verum

let p be Series of n,F_Real; :: thesis: Support p = Support |.p.|

A1: ( dom p = Bags n & Bags n = 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 )
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. F_Real & |.(p . x).| = |.p.| . x ) by Def1, POLYNOM1:def 3;

hence x in Support |.p.| by A1, POLYNOM1:def 3; :: thesis: verum

end;assume x in Support p ; :: thesis: x in Support |.p.|

then ( x in dom p & p . x <> 0. F_Real & |.(p . x).| = |.p.| . x ) by Def1, POLYNOM1:def 3;

hence x in Support |.p.| by A1, POLYNOM1:def 3; :: thesis: verum

assume x in Support |.p.| ; :: thesis: x in Support p

then ( x in dom |.p.| & |.p.| . x <> 0. F_Real & |.(p . x).| = |.p.| . x ) by Def1, POLYNOM1:def 3;

then ( x in dom p & p . x <> 0. F_Real ) by A1;

hence x in Support p by POLYNOM1:def 3; :: thesis: verum