let s be State of SCM+FSA ; :: thesis: ( IC (Initialize s) = insloc 0 & (Initialize s) . (intloc 0 ) = 1 & ( for a being read-write Int-Location holds (Initialize s) . a = s . a ) & ( for f being FinSeq-Location holds (Initialize s) . f = s . f ) & ( for l being Instruction-Location of SCM+FSA holds (Initialize s) . l = s . l ) )
dom (Start-At (insloc 0 )) = {(IC SCM+FSA )} by FUNCOP_1:19;
then ( (Start-At (insloc 0 )) . (IC SCM+FSA ) = insloc 0 & IC SCM+FSA in dom (Start-At (insloc 0 )) ) by FUNCOP_1:87, TARSKI:def 1;
hence IC (Initialize s) = insloc 0 by FUNCT_4:14; :: thesis: ( (Initialize s) . (intloc 0 ) = 1 & ( for a being read-write Int-Location holds (Initialize s) . a = s . a ) & ( for f being FinSeq-Location holds (Initialize s) . f = s . f ) & ( for l being Instruction-Location of SCM+FSA holds (Initialize s) . l = s . l ) )
A1: not intloc 0 in dom (Start-At (insloc 0 )) by SCMFSA6B:9;
A2: dom ((intloc 0 ) .--> 1) = {(intloc 0 )} by FUNCOP_1:19;
then A3: intloc 0 in dom ((intloc 0 ) .--> 1) by TARSKI:def 1;
A4: ((intloc 0 ) .--> 1) . (intloc 0 ) = 1 by FUNCOP_1:87;
thus (Initialize s) . (intloc 0 ) = (s +* ((intloc 0 ) .--> 1)) . (intloc 0 ) by A1, FUNCT_4:12
.= 1 by A3, A4, FUNCT_4:14 ; :: thesis: ( ( for a being read-write Int-Location holds (Initialize s) . a = s . a ) & ( for f being FinSeq-Location holds (Initialize s) . f = s . f ) & ( for l being Instruction-Location of SCM+FSA holds (Initialize s) . l = s . l ) )

hereby :: thesis: ( ( for f being FinSeq-Location holds (Initialize s) . f = s . f ) & ( for l being Instruction-Location of SCM+FSA holds (Initialize s) . l = s . l ) )

let a be read-write Int-Location ; :: thesis: (Initialize s) . a = s . a
A5: not a in dom (Start-At (insloc 0 )) by SCMFSA6B:9;
A6: not a in dom ((intloc 0 ) .--> 1) by A2, TARSKI:def 1;
thus (Initialize s) . a = (s +* ((intloc 0 ) .--> 1)) . a by A5, FUNCT_4:12
.= s . a by A6, FUNCT_4:12 ; :: thesis: verum

end;

hereby :: thesis: for l being Instruction-Location of SCM+FSA holds (Initialize s) . l = s . l

let f be FinSeq-Location ; :: thesis: (Initialize s) . f = s . f
A7: not f in dom (Start-At (insloc 0 )) by SCMFSA6B:10;
intloc 0 <> f by SCMFSA_2:83;
then A8: not f in dom ((intloc 0 ) .--> 1) by A2, TARSKI:def 1;
thus (Initialize s) . f = (s +* ((intloc 0 ) .--> 1)) . f by A7, FUNCT_4:12
.= s . f by A8, FUNCT_4:12 ; :: thesis: verum

end;

let l be Instruction-Location of SCM+FSA ; :: thesis: (Initialize s) . l = s . l
A9: not l in dom (Start-At (insloc 0 )) by AMI_1:137;
intloc 0 <> l by SCMFSA_2:84;
then A10: not l in dom ((intloc 0 ) .--> 1) by A2, TARSKI:def 1;
thus (Initialize s) . l = (s +* ((intloc 0 ) .--> 1)) . l by A9, FUNCT_4:12
.= s . l by A10, FUNCT_4:12 ; :: thesis: verum