let R be FinSequence of REAL ; :: thesis: for n being Element of NAT st n < len R holds
Sum (MIM (R /^ n)) = R . (n + 1)
let n be Element of 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 Def2;
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 Th29
.= R . (n + 1) by A1, A3, Def2 ;
:: thesis: verum