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 :: thesis: ( Support s = {} implies s = 0_ (X,R) )

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

now :: thesis: for x being object st x in Bags X holds
s . x = (0_ (X,R)) . x

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

end;

hence s = 0_ (X,R) ; :: thesis: verum

end;

now :: thesis: ( s = 0_ (X,R) implies Support s = {} )

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

now :: thesis: not Support s <> {}

set x = the Element of Support s;
assume Support s <> {} ; :: thesis: contradiction
then A4: 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 A4, POLYNOM1:def 4;
hence contradiction by A3, POLYNOM1:22; :: thesis: verum

end;

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

end;

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