for S being COM-Struct
for I being initial preProgram of S holds (card (stop I)) -' 1 = card I