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 = {} )

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)

end;now :: thesis: for x being object st x in Bags X holds

s . x = (0_ (X,R)) . x

hence
s = 0_ (X,R)
; :: thesis: verums . 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;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

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

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

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

hence
Support s = {}
; :: thesis: verumset 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;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