let I be Program of SCM+FSA; :: thesis: for a being Int-Location holds card (while<0 (a,I)) = (card I) + 11
let a be Int-Location ; :: thesis: card (while<0 (a,I)) = (card I) + 11
set i = ((card I) + 4) .--> (goto 0);
set C = if=0 (a,(Stop SCM+FSA),(if>0 (a,(Stop SCM+FSA),(I ';' (Goto 0)))));
set P = (if=0 (a,(Stop SCM+FSA),(if>0 (a,(Stop SCM+FSA),(I ';' (Goto 0)))))) +* (((card I) + 4) .--> (goto 0));
A1: card (if=0 (a,(Stop SCM+FSA),(if>0 (a,(Stop SCM+FSA),(I ';' (Goto 0)))))) = (card I) + 11 by Th3;
(card I) + 4 < (card I) + 11 by 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 A1, AFINSQ_1:70;
then A2: {((card I) + 4)} c= dom (if=0 (a,(Stop SCM+FSA),(if>0 (a,(Stop SCM+FSA),(I ';' (Goto 0)))))) by ZFMISC_1:37;
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 A2, XBOOLE_1:12 ;
hence card (while<0 (a,I)) = card (dom (if=0 (a,(Stop SCM+FSA),(if>0 (a,(Stop SCM+FSA),(I ';' (Goto 0)))))))
.= (card I) + 11 by A1 ;
:: thesis: verum