i in NAT by ORDINAL1:def 13;
then reconsider i = i as Instruction-Location of SCM by AMI_1:def 4;
i .--> I is NAT -defined FinPartState of SCM ;
hence i .--> I is NAT -defined FinPartState of SCM ; :: thesis: verum