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 ;
hence i .--> I is NAT -defined FinPartState of ; :: thesis: verum