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