theorem Th3: :: SCMFSA_X:3

for I being MacroInstruction of SCM+FSA
for a being Int-Location holds card (while=0 (a,I)) = (card I) + 5