let I be really-closed Program of ; :: thesis: ((Goto ((card I) + 1)) ";" I) ";" (Stop SCM+FSA) is really-closed
A1: card (I ";" (Stop SCM+FSA)) = (card I) + (card (Stop SCM+FSA)) by SCMFSA6A:21
.= (card I) + 1 by COMPOS_1:4 ;
((Goto ((card I) + 1)) ";" I) ";" (Stop SCM+FSA) = (Goto ((card I) + 1)) ";" (I ";" (Stop SCM+FSA)) by SCMFSA6A:25;
hence ((Goto ((card I) + 1)) ";" I) ";" (Stop SCM+FSA) is really-closed by Th25, A1; :: thesis: verum