let X be set ; :: thesis: for R being non empty ZeroStr holds

( not R is trivial iff ex s being Series of X,R st Support s <> {} )

let R be non empty ZeroStr ; :: thesis: ( not R is trivial iff ex s being Series of X,R st Support s <> {} )

( not R is trivial iff ex s being Series of X,R st Support s <> {} )

let R be non empty ZeroStr ; :: thesis: ( not R is trivial iff ex s being Series of X,R st Support s <> {} )

A1: now :: thesis: ( not R is trivial implies ex s being Element of bool [:(Bags X), the carrier of R:] ex s being Series of X,R st Support s <> {} )

set x = EmptyBag X;

assume not R is trivial ; :: thesis: ex s being Element of bool [:(Bags X), the carrier of R:] ex s being Series of X,R st Support s <> {}

then consider a being Element of R such that

A2: a <> 0. R ;

take s = (Bags X) --> a; :: thesis: ex s being Series of X,R st Support s <> {}

s . (EmptyBag X) = a ;

then EmptyBag X in Support s by A2, POLYNOM1:def 4;

hence ex s being Series of X,R st Support s <> {} ; :: thesis: verum

end;assume not R is trivial ; :: thesis: ex s being Element of bool [:(Bags X), the carrier of R:] ex s being Series of X,R st Support s <> {}

then consider a being Element of R such that

A2: a <> 0. R ;

take s = (Bags X) --> a; :: thesis: ex s being Series of X,R st Support s <> {}

s . (EmptyBag X) = a ;

then EmptyBag X in Support s by A2, POLYNOM1:def 4;

hence ex s being Series of X,R st Support s <> {} ; :: thesis: verum

now :: thesis: ( ex s being Series of X,R st Support s <> {} implies not R is trivial )

hence
( not R is trivial iff ex s being Series of X,R st Support s <> {} )
by A1; :: thesis: verumassume
ex s being Series of X,R st Support s <> {}
; :: thesis: not R is trivial

then consider s being Series of X,R such that

A3: Support s <> {} ;

set b = the Element of Support s;

the Element of Support s in Support s by A3;

then reconsider b = the Element of Support s as Element of Bags X ;

end;then consider s being Series of X,R such that

A3: Support s <> {} ;

set b = the Element of Support s;

the Element of Support s in Support s by A3;

then reconsider b = the Element of Support s as Element of Bags X ;

now :: thesis: for x being object holds not the carrier of R = {x}

hence
not R is trivial
by ZFMISC_1:131; :: thesis: verumgiven x being object such that A4:
the carrier of R = {x}
; :: thesis: contradiction

0. R = x by A4, TARSKI:def 1

.= s . b by A4, TARSKI:def 1 ;

hence contradiction by A3, POLYNOM1:def 4; :: thesis: verum

end;0. R = x by A4, TARSKI:def 1

.= s . b by A4, TARSKI:def 1 ;

hence contradiction by A3, POLYNOM1:def 4; :: thesis: verum