theorem Th55: :: COMPOS_1:71

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