let I be Program of SCM+FSA ; :: thesis: for a being Int-Location holds card (if>0 a,(I ';' (Goto 0 )),(Stop SCM+FSA )) = (card I) + 6
let a be Int-Location ; :: thesis: card (if>0 a,(I ';' (Goto 0 )),(Stop SCM+FSA )) = (card I) + 6
thus card (if>0 a,(I ';' (Goto 0 )),(Stop SCM+FSA )) = ((card (I ';' (Goto 0 ))) + 1) + 4 by LL, SCMFSA8B:15
.= (((card I) + (card (Goto 0 ))) + 1) + 4 by SCMFSA6A:61
.= (((card I) + 1) + 1) + 4 by SCMFSA8A:29
.= (card I) + 6 ; :: thesis: verum