let f be FinSeq-Location ; :: thesis: for s being State of SCM+FSA holds (NPP s) . f = s . f
let s be State of SCM+FSA; :: thesis: (NPP s) . f = s . f
A1: Data-Locations SCM+FSA c= dom (NPP s) by COMPOS_1:185;
f in FinSeq-Locations by SCMFSA_2:10;
then A2: f in Data-Locations SCM+FSA by SCMFSA_2:127, XBOOLE_0:def 3;
thus s . f = ((ProgramPart s) +* (NPP s)) . f by COMPOS_1:184
.= (NPP s) . f by A2, A1, FUNCT_4:14 ; :: thesis: verum