let I be set ; :: thesis: for p being Bags I -valued FinSequence
for x being object st x in I & (Sum p) . x > 0 holds
ex i being Nat st
( i in dom p & (p /. i) . x > 0 )
let p be Bags I -valued FinSequence; :: thesis: for x being object st x in I & (Sum p) . x > 0 holds
ex i being Nat st
( i in dom p & (p /. i) . x > 0 )
let x be object ; :: thesis: ( x in I & (Sum p) . x > 0 implies ex i being Nat st
( i in dom p & (p /. i) . x > 0 ) )
assume Z0: x in I ; :: thesis: ( not (Sum p) . x > 0 or ex i being Nat st
( i in dom p & (p /. i) . x > 0 ) )
assume Z1: (Sum p) . x > 0 ; :: thesis: ex i being Nat st
( i in dom p & (p /. i) . x > 0 )
defpred S₁[ object ] means for p being Bags I -valued FinSequence st p = $1 & (Sum p) . x > 0 holds
ex i being Nat st
( i in dom p & (p /. i) . x > 0 );
A1: S₁[ {} ]

proof

let p be Bags I -valued FinSequence; :: thesis: ( p = {} & (Sum p) . x > 0 implies ex i being Nat st
( i in dom p & (p /. i) . x > 0 ) )
assume p = {} ; :: thesis: ( not (Sum p) . x > 0 or ex i being Nat st
( i in dom p & (p /. i) . x > 0 ) )
then p = <*> (Bags I) ;
then Sum p = EmptyBag I by Th21;
hence ( not (Sum p) . x > 0 or ex i being Nat st
( i in dom p & (p /. i) . x > 0 ) ) by Z0, FUNCOP_1:7; :: thesis: verum

end;

A2: for p being FinSequence
for a being object st S₁[p] holds
S₁[p ^ <*a*>]

proof

let p be FinSequence; :: thesis: for a being object st S₁[p] holds
S₁[p ^ <*a*>]
let a be object ; :: thesis: ( S₁[p] implies S₁[p ^ <*a*>] )
assume Z0: S₁[p] ; :: thesis: S₁[p ^ <*a*>]
let q be Bags I -valued FinSequence; :: thesis: ( q = p ^ <*a*> & (Sum q) . x > 0 implies ex i being Nat st
( i in dom q & (q /. i) . x > 0 ) )
assume A3: q = p ^ <*a*> ; :: thesis: ( not (Sum q) . x > 0 or ex i being Nat st
( i in dom q & (q /. i) . x > 0 ) )
then reconsider p = p, aa = <*a*> as Bags I -valued FinSequence by Lem8;
len aa = 1 by FINSEQ_1:40;
then 1 in dom aa by FINSEQ_3:25;
then aa . 1 in Bags I by FUNCT_1:102;
then reconsider a = a as Element of Bags I ;
assume (Sum q) . x > 0 ; :: thesis: ex i being Nat st
( i in dom q & (q /. i) . x > 0 )
then ( ((Sum p) . x) + (a . x) = ((Sum p) + a) . x & ((Sum p) + a) . x > 0 ) by Th22, A3, PRE_POLY:def 5;

per cases then ( a . x > 0 or (Sum p) . x > 0 ) ;

suppose A4: a . x > 0 ; :: thesis: ex i being Nat st
( i in dom q & (q /. i) . x > 0 )

take i = (len p) + 1; :: thesis: ( i in dom q & (q /. i) . x > 0 )
( len q = (len p) + 1 & (len p) + 1 >= 1 ) by A3, NAT_1:11, FINSEQ_2:16;
hence i in dom q by FINSEQ_3:25; :: thesis: (q /. i) . x > 0
then q /. i = q . i by PARTFUN1:def 6;
hence (q /. i) . x > 0 by A4, A3, FINSEQ_1:42; :: thesis: verum

end;

suppose (Sum p) . x > 0 ; :: thesis: ex i being Nat st
( i in dom q & (q /. i) . x > 0 )

then consider i being Nat such that
A5: ( i in dom p & (p /. i) . x > 0 ) by Z0;
take i ; :: thesis: ( i in dom q & (q /. i) . x > 0 )
A6: dom p c= dom q by A3, FINSEQ_1:26;
hence i in dom q by A5; :: thesis: (q /. i) . x > 0
( q /. i = q . i & q . i = p . i ) by A3, A5, A6, FINSEQ_1:def 7, PARTFUN1:def 6;
hence (q /. i) . x > 0 by PARTFUN1:def 6, A5; :: thesis: verum

end;

end;

end;

for p being FinSequence holds S₁[p] from FINSEQ_1:sch 3(A1, A2);
hence ex i being Nat st
( i in dom p & (p /. i) . x > 0 ) by Z1; :: thesis: verum