let n, i be Element of NAT ; :: thesis: for r being Real st i in Seg n holds
Sum ((0* n) +* (i,r)) = r
let r be Real; :: thesis: ( i in Seg n implies Sum ((0* n) +* (i,r)) = r )
A1: len (0* n) = n by CARD_1:def 7;
reconsider w = 0* n as FinSequence of REAL ;
assume A2: i in Seg n ; :: thesis: Sum ((0* n) +* (i,r)) = r
then A3: i <= n by FINSEQ_1:1;
reconsider r = r as Element of REAL by XREAL_0:def 1;
1 <= i by A2, FINSEQ_1:1;
then i in dom (0* n) by A3, A1, FINSEQ_3:25;
then Sum (w +* (i,r)) = Sum (((w | (i -' 1)) ^ <*r*>) ^ (w /^ i)) by FUNCT_7:98
.= (Sum (((0* n) | (i -' 1)) ^ <*r*>)) + (Sum ((0* n) /^ i)) by RVSUM_1:75
.= ((Sum ((0* n) | (i -' 1))) + (Sum <*r*>)) + (Sum ((0* n) /^ i)) by RVSUM_1:75
.= ((Sum ((0* n) | (i -' 1))) + r) + (Sum ((0* n) /^ i)) by FINSOP_1:11
.= ((Sum (0* (i -' 1))) + r) + (Sum ((0* n) /^ i)) by A3, Th7, NAT_D:44
.= (0 + r) + (Sum ((0* n) /^ i)) by Th9
.= (0 + r) + (Sum (0* (n -' i))) by Th8
.= r by Th9 ;
hence Sum ((0* n) +* (i,r)) = r ; :: thesis: verum