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 3;
hence s . x = (0_ (X,R)) . x by POLYNOM1:22; :: 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:2; :: thesis: verum

end;

now

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

now

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

end;

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

end;

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