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