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 <> {} )
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;
now :: thesis: ( ex s being Series of X,R st Support s <> {} implies not R is trivial )
assume 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 ;
now :: thesis: for x being object holds not the carrier of R = {x}
given 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;
hence not R is trivial by ZFMISC_1:131; :: thesis: verum
end;
hence ( not R is trivial iff ex s being Series of X,R st Support s <> {} ) by A1; :: thesis: verum