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: S₁[ <*> REAL ] by RELAT_1:60;
A2: 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 A3: ( ( 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*>]
assume A4: 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
let i be Element of NAT ; :: thesis: ( i in dom (p ^ <*x*>) implies Sum (p ^ <*x*>) >= (p ^ <*x*>) . i )
assume A5: i in dom (p ^ <*x*>) ; :: thesis: Sum (p ^ <*x*>) >= (p ^ <*x*>) . i
A6: dom p c= dom (p ^ <*x*>) by FINSEQ_1:39;

A7: now

let n be Element of NAT ; :: thesis: ( n in dom p implies p . n >= 0 )
assume A8: n in dom p ; :: thesis: p . n >= 0
then (p ^ <*x*>) . n >= 0 by A4, A6;
hence p . n >= 0 by A8, FINSEQ_1:def 7; :: thesis: verum

end;

len (p ^ <*x*>) = (len p) + 1 by FINSEQ_2:19;
then A9: 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 ;
(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 A4;
then (p ^ <*x*>) . ((len p) + 1) >= 0 by FINSEQ_2:19;
then x >= 0 by FINSEQ_1:59;
then A10: (p . i) + x >= (p . i) + 0 by XREAL_1:8;
defpred S₂[ Element of NAT ] means Sum (p | $1) >= 0 ;
A11: S₂[ 0 ] by RVSUM_1:102;
A12: 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 A13: Sum (p | j) >= 0 ; :: thesis: S₂[j + 1]

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

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

j + 1 >= 1 by NAT_1:11;
then A15: j + 1 in dom p by A14, FINSEQ_3:27;
then p . (j + 1) >= 0 by A7;
then A16: p /. (j + 1) >= 0 by A15, PARTFUN1:def 8;
p | (j + 1) = (p | j) ^ <*(p /. (j + 1))*> by A14, JORDAN8:2;
then Sum (p | (j + 1)) = (Sum (p | j)) + (p /. (j + 1)) by RVSUM_1:104;
hence S₂[j + 1] by A13, A16; :: thesis: verum

end;

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

then j >= len p by NAT_1:13;
then ( p | j = p & p | (j + 1) = p ) by A17, FINSEQ_1:79;
hence S₂[j + 1] by A13; :: thesis: verum

end;

end;

end;

A18: for j being Element of NAT holds S₂[j] from NAT_1:sch 1(A11, A12);
p | (len p) = p by FINSEQ_1:79;
then A19: Sum p >= 0 by A18;

per cases ( i in dom p or i in {((len p) + 1)} ) by A5, A9, XBOOLE_0:def 3;

suppose A20: i in dom p ; :: thesis: Sum (p ^ <*x*>) >= (p ^ <*x*>) . i

then A21: Sum p >= p . i by A3, A7;
Sum (p ^ <*x*>) = (Sum p) + x by RVSUM_1:104;
then Sum (p ^ <*x*>) >= (p . i) + x by A21, XREAL_1:8;
then Sum (p ^ <*x*>) >= p . i by A10, XXREAL_0:2;
hence Sum (p ^ <*x*>) >= (p ^ <*x*>) . i by A20, 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 A19, XREAL_1:8;
hence Sum (p ^ <*x*>) >= (p ^ <*x*>) . i by RVSUM_1:104; :: thesis: verum

end;

end;

end;

thus for p being FinSequence of REAL holds S₁[p] from FINSEQ_2:sch 2(A1, A2); :: thesis: verum