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

proof

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

end;

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