ObjectKind l = the Instructions of S by Def14;
then reconsider L = l .--> I as FinPartState of S by Th59;
A1: l in IL by Def4;
dom L = {l} by FUNCOP_1:19;
then dom L c= IL by A1, ZFMISC_1:37;
hence l .--> I is programmed FinPartState of S by Def40; :: thesis: verum