let a be Int-Location; :: thesis: for I being MacroInstruction of SCM+FSA holds card (Times (a,I)) = (card I) + 7
let I be MacroInstruction of SCM+FSA ; :: thesis: card (Times (a,I)) = (card I) + 7
card (I ";" (SubFrom (a,(intloc 0)))) = (card I) + 2 by SCMFSA6A:34;
hence card (Times (a,I)) = ((card I) + 2) + 5 by SCMFSA_X:4
.= (card I) + 7 ;
:: thesis: verum