let I be set ; :: thesis: for p being Bags I -valued FinSequence st Sum p = EmptyBag I & ( for a being bag of I st a in rng p holds
a <> EmptyBag I ) holds
p = {}
let p be Bags I -valued FinSequence; :: thesis: ( Sum p = EmptyBag I & ( for a being bag of I st a in rng p holds
a <> EmptyBag I ) implies p = {} )
assume Z0: Sum p = EmptyBag I ; :: thesis: ( ex a being bag of I st
( a in rng p & not a <> EmptyBag I ) or p = {} )
assume Z1: for a being bag of I st a in rng p holds
a <> EmptyBag I ; :: thesis: p = {}
assume p <> {} ; :: thesis: contradiction
then consider a being object such that
A1: a in rng p by XBOOLE_0:7;
rng p c= Bags I by RELAT_1:def 19;
then reconsider a = a as Element of Bags I by A1;
consider x being object such that
A2: ( x in I & a . x <> (EmptyBag I) . x ) by A1, Z1, PBOOLE:def 10;
A4: (EmptyBag I) . x = 0 by A2, FUNCOP_1:7;
then A3: a . x > 0 by A2;
thus contradiction by A4, A3, Z0, A1, Th26, PRE_POLY:def 11; :: thesis: verum