theorem Th20: :: TURING_1:20

for f being FinSequence of NAT
for s being Element of NAT st len f >= 1 holds
( Sum (Prefix ((<*s*> ^ f),1)) = s & Sum (Prefix ((<*s*> ^ f),2)) = s + (f /. 1) )