set J = Stop SCM+FSA ;
let a be Int-Location ; :: thesis: for I being Program of SCM+FSA holds (while=0 a,I) . ((card I) + 4) = goto 0
let I be Program of SCM+FSA ; :: 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:19;
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 Th13, 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:87 ;
:: thesis: verum