let R be real-valued FinSequence; :: thesis: for n being Nat st n < len R holds
Sum (MIM (R /^ n)) = R . (n + 1)
let n be Nat; :: thesis: ( n < len R implies Sum (MIM (R /^ n)) = R . (n + 1) )
assume A1: n < len R ; :: thesis: Sum (MIM (R /^ n)) = R . (n + 1)
then A2: len (R /^ n) = (len R) - n by Def1;
n + 1 <= len R by A1, NAT_1:13;
then 1 <= (len R) - n by XREAL_1:19;
then A3: 1 in dom (R /^ n) by A2, FINSEQ_3:25;
len (R /^ n) <> 0 by A1, A2;
hence Sum (MIM (R /^ n)) = (R /^ n) . 1 by Th16
.= R . (n + 1) by A1, A3, Def1 ;
:: thesis: verum