set J = (intloc 0 ) .--> 1;
A1: dom ((intloc 0 ) .--> 1) = {(intloc 0 )} by FUNCOP_1:19;
reconsider J = (intloc 0 ) .--> 1 as finite Function ;
A2: dom the Object-Kind of SCM+FSA = the carrier of SCM+FSA by FUNCT_2:def 1;

now

let x be set ; :: thesis: ( x in dom J implies J . x in the Object-Kind of SCM+FSA . x )
intloc 0 in Int-Locations by SCMFSA_2:9;
then A3: dom J c= Int-Locations by A1, ZFMISC_1:37;
assume A4: x in dom J ; :: thesis: J . x in the Object-Kind of SCM+FSA . x
then reconsider l = x as Int-Location by A3, SCMFSA_2:11;
A5: the Object-Kind of SCM+FSA . l = ObjectKind l
.= INT by SCMFSA_2:26 ;
A6: J . x in rng J by A4, FUNCT_1:def 5;
A7: 1 in INT by INT_1:def 2;
A8: rng J = {1} by FUNCOP_1:14;
{1} c= INT by A7, ZFMISC_1:37;
hence J . x in the Object-Kind of SCM+FSA . x by A5, A6, A8; :: thesis: verum

end;

then reconsider J = J as FinPartState of SCM+FSA by A1, A2, CARD_3:def 9;
(I +* J) +* (Start-At (insloc 0 )) is FinPartState of SCM+FSA ;
hence (I +* ((intloc 0 ) .--> 1)) +* (Start-At (insloc 0 )) is FinPartState of SCM+FSA ; :: thesis: verum