consider s being State of S;
A1: ObjectKind l = the Instructions of S by AMI_1:def 14;
( l in IL & ObjectKind (IC S) = IL ) by AMI_1:def 4, AMI_1:def 11;
then reconsider f = (IC S),l --> l,i as FinPartState of S by A1, AMI_1:58;
IC (Following (s +* f)) in NIC i,l by Lm2;
hence not NIC i,l is empty ; :: thesis: verum