theorem Th6: :: SCMP_GCD:6

for i being Instruction of SCMPDS
for I being Program of SCMPDS holds
( (I ';' i) . (card I) = i & card I in dom (I ';' i) )