let p be PartState of SCM+FSA; :: thesis: (Initialized p) . (intloc 0) = 1
A1: ((intloc 0) .--> 1) . (intloc 0) = 1 by FUNCOP_1:72;
A2: Initialized p = Initialize (p +* ((intloc 0) .--> 1)) by FUNCT_4:14;
A3: intloc 0 in dom ((intloc 0) .--> 1) by TARSKI:def 1;
not intloc 0 in dom (Start-At (0,SCM+FSA)) by SCMFSA_2:102;
hence (Initialized p) . (intloc 0) = (p +* ((intloc 0) .--> 1)) . (intloc 0) by A2, FUNCT_4:11
.= 1 by A3, A1, FUNCT_4:13 ;
:: thesis: verum