let X be set ; :: thesis: for R being non empty ZeroStr
for s being Series of X,R holds
( s = 0_ (X,R) iff Support s = {} )
let R be non empty ZeroStr ; :: thesis: for s being Series of X,R holds
( s = 0_ (X,R) iff Support s = {} )
let s be Series of X,R; :: thesis: ( s = 0_ (X,R) iff Support s = {} )

A1: now

assume A2: Support s = {} ; :: thesis: s = 0_ (X,R)

A3: now

let x be set ; :: thesis: ( x in Bags X implies s . x = (0_ (X,R)) . x )
assume x in Bags X ; :: thesis: s . x = (0_ (X,R)) . x
then reconsider x9 = x as Element of Bags X ;
s . x9 = 0. R by A2, POLYNOM1:def 9;
hence s . x = (0_ (X,R)) . x by POLYNOM1:81; :: thesis: verum

end;

( dom s = Bags X & dom (0_ (X,R)) = Bags X ) by FUNCT_2:def 1;
hence s = 0_ (X,R) by A3, FUNCT_1:9; :: thesis: verum

end;

now

assume A4: s = 0_ (X,R) ; :: thesis: Support s = {}

now

consider x being Element of Support s;
assume Support s <> {} ; :: thesis: contradiction
then A5: x in Support s ;
then reconsider x = x as bag of X ;
s . x <> 0. R by A5, POLYNOM1:def 9;
hence contradiction by A4, POLYNOM1:81; :: thesis: verum

end;

hence Support s = {} ; :: thesis: verum

end;

hence ( s = 0_ (X,R) iff Support s = {} ) by A1; :: thesis: verum