let R be FinSequence of REAL ; :: 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

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