let p be natural-valued FinSequence; :: thesis: for i being Nat st i in dom p holds
Sum p >= p . i
let i be Nat; :: thesis: ( i in dom p implies Sum p >= p . i )
A0: p is FinSequence of NAT by FINSEQ_1:103;
defpred S₁[ FinSequence of NAT ] means for i being Element of NAT st i in dom $1 holds
Sum $1 >= $1 . i;
A1: for p being FinSequence of NAT
for x being Element of NAT st S₁[p] holds
S₁[p ^ <*x*>]

proof

let p be FinSequence of NAT ; :: thesis: for x being Element of NAT st S₁[p] holds
S₁[p ^ <*x*>]
let x be Element of NAT ; :: thesis: ( S₁[p] implies S₁[p ^ <*x*>] )
assume A2: for i being Element of NAT st i in dom p holds
Sum p >= p . i ; :: thesis: S₁[p ^ <*x*>]
let i be Element of NAT ; :: thesis: ( i in dom (p ^ <*x*>) implies Sum (p ^ <*x*>) >= (p ^ <*x*>) . i )
A3: (p . i) + x >= p . i by NAT_1:11;
len (p ^ <*x*>) = (len p) + 1 by FINSEQ_2:16;
then A4: 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 ;
assume A5: 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 A5, A4, XBOOLE_0:def 3;

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

then (Sum p) + x >= (p . i) + x by A2, XREAL_1:6;
then Sum (p ^ <*x*>) >= (p . i) + x by RVSUM_1:74;
then Sum (p ^ <*x*>) >= p . i by A3, XXREAL_0:2;
hence Sum (p ^ <*x*>) >= (p ^ <*x*>) . i by A6, 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 >= (p ^ <*x*>) . i by NAT_1:11;
hence Sum (p ^ <*x*>) >= (p ^ <*x*>) . i by RVSUM_1:74; :: thesis: verum

end;

end;

end;

A7: S₁[ <*> NAT] ;
for p being FinSequence of NAT holds S₁[p] from FINSEQ_2:sch 2(A7, A1);
hence ( i in dom p implies Sum p >= p . i ) by A0; :: thesis: verum