not intloc 0 in dom (Start-At (0,SCM+FSA)) by SCMFSA_2:102;
hence (Initialize ((intloc 0) .--> 1)) . (intloc 0) = ((intloc 0) .--> 1) . (intloc 0) by FUNCT_4:11
.= 1 by FUNCOP_1:72 ;
:: thesis: verum