set J = Stop SCM+FSA;
let a be Int-Location ; :: thesis: for I being Program of holds (while>0 (a,I)) . ((card I) + 4) = goto 0
let I be Program of ; :: thesis: (while>0 (a,I)) . ((card I) + 4) = goto 0
set I1 = I ';' (Goto 0);
set f = ((card I) + 4) .--> (goto 0);
set Lc4 = (card I) + 4;
dom (((card I) + 4) .--> (goto 0)) = {((card I) + 4)} by FUNCOP_1:13;
then A1: (card I) + 4 in dom (((card I) + 4) .--> (goto 0)) by TARSKI:def 1;
( (card I) + 4 in dom (while>0 (a,I)) & dom (while>0 (a,I)) = (dom (if>0 (a,(I ';' (Goto 0)),(Stop SCM+FSA)))) \/ (dom (((card I) + 4) .--> (goto 0))) ) by Th38, FUNCT_4:def 1;
hence (while>0 (a,I)) . ((card I) + 4) = (((card I) + 4) .--> (goto 0)) . ((card I) + 4) by A1, FUNCT_4:def 1
.= goto 0 by FUNCOP_1:72 ;
:: thesis: verum