let X be Ordinal; :: thesis: for S being non empty ZeroStr
for p being Series of X,S holds
( vars p = {} iff p is Constant )
let S be non empty ZeroStr ; :: thesis: for p being Series of X,S holds
( vars p = {} iff p is Constant )
let p be Series of X,S; :: thesis: ( vars p = {} iff p is Constant )
thus ( vars p = {} implies p is Constant ) :: thesis: ( p is Constant implies vars p = {} )

proof

assume A1: vars p = {} ; :: thesis: p is Constant
assume not p is Constant ; :: thesis: contradiction
then consider b being bag of X such that
A2: ( b <> EmptyBag X & p . b <> 0. S ) by POLYNOM7:def 7;
( b in Bags X & Bags X = dom p ) by PARTFUN1:def 2, PRE_POLY:def 12;
then A3: b in Support p by A2, POLYNOM1:def 4;
( dom b = X & X = dom (EmptyBag X) ) by PARTFUN1:def 2;
then ex x being object st
( x in X & (EmptyBag X) . x <> b . x ) by A2;
hence contradiction by A1, A3, Def5; :: thesis: verum

end;

assume A4: p is Constant ; :: thesis: vars p = {}
assume vars p <> {} ; :: thesis: contradiction
then consider x being object such that
A5: x in vars p by XBOOLE_0:def 1;
consider b being bag of X such that
A6: ( b in Support p & b . x <> 0 ) by A5, Def5;
( p . b <> 0. S & b <> EmptyBag X ) by A6, POLYNOM1:def 4;
hence contradiction by A4, POLYNOM7:def 7; :: thesis: verum