theorem Th4: :: TURING_1:4

for x1, x2 being Element of NAT holds
( Sum (Prefix (<*x1,x2*>,1)) = x1 & Sum (Prefix (<*x1,x2*>,2)) = x1 + x2 )