let p be PartState of SCM+FSA; ( IC (Initialized p) = 0 & (Initialized p) . (intloc 0) = 1 )
A1:
((intloc 0) .--> 1) . (intloc 0) = 1
by FUNCOP_1:87;
dom (Start-At (0,SCM+FSA)) = {(IC )}
by FUNCOP_1:19;
then A2:
IC in dom (Start-At (0,SCM+FSA))
by TARSKI:def 1;
A3:
Initialized p = Initialize (p +* ((intloc 0) .--> 1))
by FUNCT_4:15;
(Start-At (0,SCM+FSA)) . (IC ) = 0
by FUNCOP_1:87;
hence
IC (Initialized p) = 0
by A2, FUNCT_4:14, A3; (Initialized p) . (intloc 0) = 1
dom ((intloc 0) .--> 1) = {(intloc 0)}
by FUNCOP_1:19;
then A5:
intloc 0 in dom ((intloc 0) .--> 1)
by TARSKI:def 1;
not intloc 0 in dom (Start-At (0,SCM+FSA))
by SCMFSA_2:130;
hence (Initialized p) . (intloc 0) =
(p +* ((intloc 0) .--> 1)) . (intloc 0)
by FUNCT_4:12, A3
.=
1
by A5, A1, FUNCT_4:14
;
verum