defpred S1[ FinSequence of REAL ] means ( ( for n being Element of NAT st n in dom $1 holds
$1 . n >= 0 ) implies for i being Element of NAT st i in dom $1 holds
Sum $1 >= $1 . i );
A1: for p being FinSequence of REAL
for x being Element of REAL st S1[p] holds
S1[p ^ <*x*>]
proof
let p be FinSequence of REAL ; :: thesis: for x being Element of REAL st S1[p] holds
S1[p ^ <*x*>]
let x be Element of REAL ; :: thesis: ( S1[p] implies S1[p ^ <*x*>] )
assume A2: ( ( for n being Element of NAT st n in dom p holds
p . n >= 0 ) implies for i being Element of NAT st i in dom p holds
Sum p >= p . i ) ; :: thesis: S1[p ^ <*x*>]
defpred S2[ Nat] means Sum (p | $1) >= 0 ;
assume A3: for n being Element of NAT st n in dom (p ^ <*x*>) holds
(p ^ <*x*>) . n >= 0 ; :: thesis: for i being Element of NAT st i in dom (p ^ <*x*>) holds
Sum (p ^ <*x*>) >= (p ^ <*x*>) . i
A4: dom p c= dom (p ^ <*x*>) by FINSEQ_1:26;
A5: now :: thesis: for n being Element of NAT st n in dom p holds
p . n >= 0
let n be Element of NAT ; :: thesis: ( n in dom p implies p . n >= 0 )
assume A6: n in dom p ; :: thesis: p . n >= 0
then (p ^ <*x*>) . n >= 0 by A3, A4;
hence p . n >= 0 by A6, FINSEQ_1:def 7; :: thesis: verum
end;
A7: for j being Nat st S2[j] holds
S2[j + 1]
proof
let j be Nat; :: thesis: ( S2[j] implies S2[j + 1] )
assume A8: Sum (p | j) >= 0 ; :: thesis: S2[j + 1]
per cases ( j + 1 <= len p or j + 1 > len p ) ;
suppose A9: j + 1 <= len p ; :: thesis: S2[j + 1]
then p | (j + 1) = (p | j) ^ <*(p /. (j + 1))*> by FINSEQ_5:82;
then A10: Sum (p | (j + 1)) = (Sum (p | j)) + (p /. (j + 1)) by RVSUM_1:74;
j + 1 >= 1 by NAT_1:11;
then A11: j + 1 in dom p by A9, FINSEQ_3:25;
then p . (j + 1) >= 0 by A5;
then p /. (j + 1) >= 0 by A11, PARTFUN1:def 6;
hence S2[j + 1] by A8, A10; :: thesis: verum
end;
end;
end;
let i be Element of NAT ; :: thesis: ( i in dom (p ^ <*x*>) implies Sum (p ^ <*x*>) >= (p ^ <*x*>) . i )
(len p) + 1 >= 0 + 1 by XREAL_1:6;
then len (p ^ <*x*>) >= 1 by FINSEQ_2:16;
then len (p ^ <*x*>) in dom (p ^ <*x*>) by FINSEQ_3:25;
then (p ^ <*x*>) . (len (p ^ <*x*>)) >= 0 by A3;
then (p ^ <*x*>) . ((len p) + 1) >= 0 by FINSEQ_2:16;
then x >= 0 by FINSEQ_1:42;
then A13: (p . i) + x >= (p . i) + 0 by XREAL_1:6;
A14: p | (len p) = p by FINSEQ_1:58;
len (p ^ <*x*>) = (len p) + 1 by FINSEQ_2:16;
then A15: dom (p ^ <*x*>) = Seg ((len p) + 1) by FINSEQ_1:def 3
.= (Seg (len p)) \/ {((len p) + 1)} by FINSEQ_1:9
.= (dom p) \/ {((len p) + 1)} by FINSEQ_1:def 3 ;
A16: S2[ 0 ] by RVSUM_1:72;
for j being Nat holds S2[j] from NAT_1:sch 2(A16, A7);
 then A17: Sum p >= 0 by A14;
assume A18: i in dom (p ^ <*x*>) ; :: thesis: Sum (p ^ <*x*>) >= (p ^ <*x*>) . i
per cases ( i in dom p or i in {((len p) + 1)} ) by A18, A15, XBOOLE_0:def 3;
suppose A19: i in dom p ; :: thesis: Sum (p ^ <*x*>) >= (p ^ <*x*>) . i
A20: Sum (p ^ <*x*>) = (Sum p) + x by RVSUM_1:74;
Sum p >= p . i by A2, A5, A19;
then Sum (p ^ <*x*>) >= (p . i) + x by A20, XREAL_1:6;
then Sum (p ^ <*x*>) >= p . i by A13, XXREAL_0:2;
hence Sum (p ^ <*x*>) >= (p ^ <*x*>) . i by A19, FINSEQ_1:def 7; :: thesis: verum
end;
suppose i in {((len p) + 1)} ; :: thesis: Sum (p ^ <*x*>) >= (p ^ <*x*>) . i
then i = (len p) + 1 by TARSKI:def 1;
then (p ^ <*x*>) . i = x by FINSEQ_1:42;
then (Sum p) + x >= 0 + ((p ^ <*x*>) . i) by A17, XREAL_1:6;
hence Sum (p ^ <*x*>) >= (p ^ <*x*>) . i by RVSUM_1:74; :: thesis: verum
end;
end;
end;
A21: S1[ <*> REAL] ;
thus for p being FinSequence of REAL holds S1[p] from FINSEQ_2:sch 2(A21, A1); :: thesis: verum