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

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