theorem Th57: :: COMPOS_1:73

for S being COM-Struct
for I being Program of S holds LastLoc (stop I) = card I