let S be COM-Struct ; :: thesis: for I being initial preProgram of S holds (card (stop I)) -' 1 = card I
let I be initial preProgram of S; :: thesis: (card (stop I)) -' 1 = card I
thus (card (stop I)) -' 1 = (card (stop I)) - 1 by PRE_CIRC:20
.= ((card I) + (card (Stop S))) - 1 by AFINSQ_1:17
.= ((card I) + 1) - 1 by AFINSQ_1:34
.= card I ; :: thesis: verum