set C = if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA );
set i = (insloc ((card I) + 4)) .--> (goto (insloc 0 ));
set P = (if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA )) +* ((insloc ((card I) + 4)) .--> (goto (insloc 0 )));
( card (if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA )) = (card I) + 6 & (card I) + 4 < (card I) + 6 ) by Th2, XREAL_1:8;
then insloc ((card I) + 4) in dom (if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA )) by SCMFSA6A:15;
then A3: {(insloc ((card I) + 4))} c= dom (if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA )) by ZFMISC_1:37;
A4: dom ((if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA )) +* ((insloc ((card I) + 4)) .--> (goto (insloc 0 )))) = (dom (if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA ))) \/ (dom ((insloc ((card I) + 4)) .--> (goto (insloc 0 )))) by FUNCT_4:def 1
.= (dom (if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA ))) \/ {(insloc ((card I) + 4))} by FUNCOP_1:19
.= dom (if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA )) by A3, XBOOLE_1:12 ;
(if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA )) +* ((insloc ((card I) + 4)) .--> (goto (insloc 0 ))) is initial

proof

let m, n be Nat; :: according to SCMNORM:def 1 :: thesis: ( not n in dom ((if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA )) +* ((insloc ((card I) + 4)) .--> (goto (insloc 0 )))) or n <= m or m in dom ((if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA )) +* ((insloc ((card I) + 4)) .--> (goto (insloc 0 )))) )
thus ( not n in dom ((if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA )) +* ((insloc ((card I) + 4)) .--> (goto (insloc 0 )))) or n <= m or m in dom ((if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA )) +* ((insloc ((card I) + 4)) .--> (goto (insloc 0 )))) ) by A4, SCMNORM:def 1; :: thesis: verum

end;

hence (if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA )) +* ((insloc ((card I) + 4)) .--> (goto (insloc 0 ))) is Program of SCM+FSA ; :: thesis: verum