for p being preProgram of SCM+FSA holds not First*NotUsed p in UsedI*Loc p