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

set x = EmptyBag X;
assume A2: not R is trivial ; :: thesis: ex s, s being Series of X,R st Support s <> {}

now

assume A3: for a being Element of R holds not a <> 0. R ; :: thesis: contradiction
ex x being set st the carrier of R = {x}

proof

take 0. R ; :: thesis: the carrier of R = {(0. R)}

A4: now

let u be set ; :: thesis: ( u in the carrier of R implies u in {(0. R)} )
assume u in the carrier of R ; :: thesis: u in {(0. R)}
then u = 0. R by A3;
hence u in {(0. R)} by TARSKI:def 1; :: thesis: verum

end;

for u being set st u in {(0. R)} holds
u in the carrier of R ;
hence the carrier of R = {(0. R)} by A4, TARSKI:2; :: thesis: verum

end;

hence contradiction by A2, REALSET1:def 4; :: thesis: verum

end;

then consider a being Element of R such that
A5: a <> 0. R ;
set s = (Bags X) --> a;
reconsider s = (Bags X) --> a as Function of (Bags X),the carrier of R ;
reconsider s = s as Function of (Bags X),R ;
reconsider s = s as Series of X,R ;
take s = s; :: thesis: ex s being Series of X,R st Support s <> {}
s . (EmptyBag X) = a by FUNCOP_1:13;
then EmptyBag X in Support s by A5, POLYNOM1:def 9;
hence ex s being Series of X,R st Support s <> {} ; :: thesis: verum

end;

now

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
A6: Support s <> {} ;
consider b being Element of Support s;
b in Support s by A6;
then reconsider b = b as Element of Bags X ;

now

assume ex x being set st the carrier of R = {x} ; :: thesis: contradiction
then consider x being set such that
A7: the carrier of R = {x} ;
0. R = x by A7, TARSKI:def 1
.= s . b by A7, TARSKI:def 1 ;
hence contradiction by A6, POLYNOM1:def 9; :: thesis: verum

end;

hence not R is trivial by REALSET1:def 4; :: thesis: verum

end;

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