let i be Instruction of SCM+FSA; :: thesis: ( i is sequential implies i is No-StopCode )
assume A1: i is sequential ; :: thesis: i is No-StopCode
reconsider i = i as Element of the InstructionsF of SCM+FSA ;
i <> halt SCM+FSA by A1;
then i is No-StopCode by COMPOS_0:def 12;
hence i is No-StopCode ; :: thesis: verum