let I be really-closed MacroInstruction of SCM+FSA ; :: thesis: for k being Nat st k <= card I holds

(Goto k) ";" I is really-closed

let k be Nat; :: thesis: ( k <= card I implies (Goto k) ";" I is really-closed )

(Goto k) ";" I = (Macro (goto k)) ';' I by SCMFSA8A:43;

hence ( k <= card I implies (Goto k) ";" I is really-closed ) by Th24; :: thesis: verum

(Goto k) ";" I is really-closed

let k be Nat; :: thesis: ( k <= card I implies (Goto k) ";" I is really-closed )

(Goto k) ";" I = (Macro (goto k)) ';' I by SCMFSA8A:43;

hence ( k <= card I implies (Goto k) ";" I is really-closed ) by Th24; :: thesis: verum