defpred S1[ 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 S1[p] holds
S1[p ^ <*x*>]
proof
let p be FinSequence of NAT ; :: thesis: for x being Element of NAT st S1[p] holds
S1[p ^ <*x*>]
let x be Element of NAT ; :: thesis: ( S1[p] implies S1[p ^ <*x*>] )
assume A2: for i being Element of NAT st i in dom p holds
Sum p >= p . i ; :: thesis: S1[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 >= p . i by A2;
then (Sum p) + x >= (p . i) + x by 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: S1[ <*> NAT] ;
thus for p being FinSequence of NAT holds S1[p] from FINSEQ_2:sch 2(A7, A1); :: thesis: verum