let r be Real; :: thesis: for F being FinSequence of REAL st ( for n being Nat st n in dom F holds
F . n = r ) holds
Sum F = r * (len F)
let F be FinSequence of REAL ; :: thesis: ( ( for n being Nat st n in dom F holds
F . n = r ) implies Sum F = r * (len F) )
assume for n being Nat st n in dom F holds
F . n = r ; :: thesis: Sum F = r * (len F)
then for z being object st z in dom F holds
F . z = r ;
then F = (dom F) --> r by FUNCOP_1:11;
then F = (Seg (len F)) --> r by FINSEQ_1:def 3;
then F = (len F) |-> r by FINSEQ_2:def 2;
hence Sum F = r * (len F) by RVSUM_1:80; :: thesis: verum