for r being Real
for n being non zero Nat ex f being FinSequence of REAL st
( len f = n & Sum f = r )