defpred S₁[ 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 S₁[p] holds
S₁[p ^ <*x*>]

proof

let p be FinSequence of REAL ; :: thesis: for x being Element of REAL st S₁[p] holds
S₁[p ^ <*x*>]
let x be Element of REAL ; :: thesis: ( S₁[p] implies S₁[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: S₁[p ^ <*x*>]
defpred S₂[ Element of 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:39;

A5: now

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 Element of NAT st S₂[j] holds
S₂[j + 1]

proof

let j be Element of NAT ; :: thesis: ( S₂[j] implies S₂[j + 1] )
assume A8: Sum (p | j) >= 0 ; :: thesis: S₂[j + 1]

per cases ( j + 1 <= len p or j + 1 > len p ) ;

suppose A9: j + 1 <= len p ; :: thesis: S₂[j + 1]

then p | (j + 1) = (p | j) ^ <*(p /. (j + 1))*> by FINSEQ_5:85;
then A10: Sum (p | (j + 1)) = (Sum (p | j)) + (p /. (j + 1)) by RVSUM_1:104;
j + 1 >= 1 by NAT_1:11;
then A11: j + 1 in dom p by A9, FINSEQ_3:27;
then p . (j + 1) >= 0 by A5;
then p /. (j + 1) >= 0 by A11, PARTFUN1:def 8;
hence S₂[j + 1] by A8, A10; :: thesis: verum

end;

suppose A12: j + 1 > len p ; :: thesis: S₂[j + 1]

then j >= len p by NAT_1:13;
then p | j = p by FINSEQ_1:79;
hence S₂[j + 1] by A8, A12, FINSEQ_1:79; :: 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:8;
then len (p ^ <*x*>) >= 1 by FINSEQ_2:19;
then len (p ^ <*x*>) in dom (p ^ <*x*>) by FINSEQ_3:27;
then (p ^ <*x*>) . (len (p ^ <*x*>)) >= 0 by A3;
then (p ^ <*x*>) . ((len p) + 1) >= 0 by FINSEQ_2:19;
then x >= 0 by FINSEQ_1:59;
then A13: (p . i) + x >= (p . i) + 0 by XREAL_1:8;
A14: p | (len p) = p by FINSEQ_1:79;
len (p ^ <*x*>) = (len p) + 1 by FINSEQ_2:19;
then A15: dom (p ^ <*x*>) = Seg ((len p) + 1) by FINSEQ_1:def 3
.= (Seg (len p)) \/ {((len p) + 1)} by FINSEQ_1:11
.= (dom p) \/ {((len p) + 1)} by FINSEQ_1:def 3 ;
A16: S₂[ 0 ] by RVSUM_1:102;
for j being Element of NAT holds S₂[j] from NAT_1:sch 1(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:104;
Sum p >= p . i by A2, A5, A19;
then Sum (p ^ <*x*>) >= (p . i) + x by A20, XREAL_1:8;
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:59;
then (Sum p) + x >= 0 + ((p ^ <*x*>) . i) by A17, XREAL_1:8;
hence Sum (p ^ <*x*>) >= (p ^ <*x*>) . i by RVSUM_1:104; :: thesis: verum

end;

end;

end;

A21: S₁[ <*> REAL ] by RELAT_1:60;
thus for p being FinSequence of REAL holds S₁[p] from FINSEQ_2:sch 2(A21, A1); :: thesis: verum