let I be Instruction of S; :: thesis: ( I is sequential implies I is ins-loc-free )

assume I is sequential ; :: thesis: I is ins-loc-free

then A1: JUMP I is empty by AMISTD_1:13;

rng (JumpPart I) = JUMP I by Def1;

hence JumpPart I is empty by A1; :: according to COMPOS_0:def 8 :: thesis: verum

assume I is sequential ; :: thesis: I is ins-loc-free

then A1: JUMP I is empty by AMISTD_1:13;

rng (JumpPart I) = JUMP I by Def1;

hence JumpPart I is empty by A1; :: according to COMPOS_0:def 8 :: thesis: verum