A1: now

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

end;

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