theorem Th17: :: IRRAT_1:17

for sq being FinSequence of REAL st len sq > 0 holds
Sum sq = (sq . 1) + (Sum (sq /^ 1))