let f be constant non empty real-valued FinSequence; :: thesis: Sum f = (the_value_of f) * (len f)
set r = the_value_of f;
set i = len f;
f = (dom f) --> (the_value_of f) by FUNCOP_1:80
.= (len f) |-> (the_value_of f) by FINSEQ_1:def 3 ;
hence Sum f = (the_value_of f) * (len f) by RVSUM_1:80; :: thesis: verum