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: now

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

end;

reconsider J = J as FinPartState of SCM+FSA by A1, A2, FUNCT_1:def 20, RELAT_1:def 18;
(I +* J) +* (Start-At 0 ,SCM+FSA ) is PartState of SCM+FSA ;
hence (I +* ((intloc 0 ) .--> 1)) +* (Start-At 0 ,SCM+FSA ) is PartState of SCM+FSA ; :: thesis: verum