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

proof

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

end;

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