let r be Real; :: thesis: for n being non zero Nat ex f being FinSequence of REAL st
( len f = n & Sum f = r )
let n be non zero Nat; :: thesis: ex f being FinSequence of REAL st
( len f = n & Sum f = r )
reconsider k = n - 1 as Nat ;
0 in REAL by XREAL_0:def 1;
then reconsider g = k |-> 0 as FinSequence of REAL by FINSEQ_2:63;
reconsider h = g ^ <*r*> as FinSequence of REAL by RVSUM_1:145;
A1: len (g ^ <*r*>) = (len g) + 1 by FINSEQ_2:16
.= k + 1 ;
Sum (g ^ <*r*>) = (Sum (k |-> 0)) + r by RVSUM_1:74
.= 0 + r ;
then ( Sum h = r & len h = k + 1 ) by A1;
hence ex f being FinSequence of REAL st
( len f = n & Sum f = r ) ; :: thesis: verum