theorem :: COMPOS_1:72

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