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