theorem Th21: :: TURING_1:21

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