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
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. F_Real & |.(p . x).| = |.p.| . x ) by Def1, 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. 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