X: l in NAT ;
NAT c= the carrier of S by Def3;
then reconsider la = l as Object of S by X;
the Object-Kind of S . l = the Instructions of S by Def14;
then reconsider L = la .--> I as PartState of S by Th59;
( l in NAT & dom L = {l} ) by FUNCOP_1:19;
hence l .--> I is NAT -defined FinPartState of by RELAT_1:def 18; :: thesis: verum