ObjectKind l = the Instructions of S by Def14;
then reconsider L = l .--> I as FinPartState of S by Th59;
( l in NAT & dom L = {l} ) by Def4, FUNCOP_1:19;
then dom L c= NAT by ZFMISC_1:37;
hence l .--> I is NAT -defined FinPartState of S by RELAT_1:def 18; :: thesis: verum