let k be Nat; :: thesis: for f being complex-valued Function holds (f,k) +...+ (f,k) = f . k
let f be complex-valued Function; :: thesis: (f,k) +...+ (f,k) = f . k
consider h being complex-valued FinSequence such that
A1: ( (f,k) +...+ (f,k) = Sum h & len h = (k -' k) + 1 & h . (0 + 1) = f . (0 + k) & ... & h . ((k -' k) + 1) = f . ((k -' k) + k) ) by Th9;
(k -' k) + 1 = 0 + 1 by XREAL_1:232;
then h = <*(h . 1)*> by A1, FINSEQ_1:40;
then Sum h = h . 1 by RVSUM_2:30;
hence (f,k) +...+ (f,k) = f . k by A1; :: thesis: verum