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 ;
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:
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 ;
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