let i, n be Nat; :: thesis: for f1, f2 being natural-valued FinSequence st len f1 = i + 1 & f1 | i = f2 holds
Sum (n |^ f1) = (Sum (n |^ f2)) + (n |^ (f1 . (i + 1)))
let f1, f2 be natural-valued FinSequence; :: thesis: ( len f1 = i + 1 & f1 | i = f2 implies Sum (n |^ f1) = (Sum (n |^ f2)) + (n |^ (f1 . (i + 1))) )
assume A1: ( len f1 = i + 1 & f1 | i = f2 ) ; :: thesis: Sum (n |^ f1) = (Sum (n |^ f2)) + (n |^ (f1 . (i + 1)))
set i1 = i + 1;
f1 = (f1 | i) ^ <*(f1 . (i + 1))*> by A1, FINSEQ_3:55;
then n |^ f1 = (n |^ f2) ^ (n |^ <*(f1 . (i + 1))*>) by Th24, A1
.= (n |^ f2) ^ <*(n to_power (f1 . (i + 1)))*> by Th23 ;
hence Sum (n |^ f1) = (Sum (n |^ f2)) + (n |^ (f1 . (i + 1))) by RVSUM_1:74; :: thesis: verum