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

now

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

end;

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

end;

now

assume A5: Support s = {} ; :: thesis: s = 0_ X,R
A6: ( dom s = Bags X & dom (0_ X,R) = Bags X ) by FUNCT_2:def 1;

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 x' = x as Element of Bags X ;
s . x' = 0. R by A5, POLYNOM1:def 9;
hence s . x = (0_ X,R) . x by POLYNOM1:81; :: thesis: verum

end;

hence s = 0_ X,R by A6, FUNCT_1:9; :: thesis: verum

end;

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