theorem Th7: :: SCMFSA10:7

for a being Int-Location
for il being Nat holds a =0_goto il = [7,<*il*>,<*a*>]