set D = Int-Locations \/ FinSeq-Locations ;
set A = NAT ;
let s be State of SCM+FSA ; :: thesis: for I being Program of SCM+FSA holds IExec I,s = IExec I,(Initialize s)
let I be Program of SCM+FSA ; :: thesis: IExec I,s = IExec I,(Initialize s)
dom s = ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) \/ NAT by SCMFSA6A:34;
then A1: NAT c= dom s by XBOOLE_1:7;
dom (Initialize s) = ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) \/ NAT by SCMFSA6A:34;
then A2: NAT c= dom (Initialize s) by XBOOLE_1:7;
for x being set st x in NAT holds
s . x = (Initialize s) . x

proof

let x be set ; :: thesis: ( x in NAT implies s . x = (Initialize s) . x )
assume x in NAT ; :: thesis: s . x = (Initialize s) . x
then reconsider x = x as Instruction-Location of SCM+FSA by AMI_1:def 4;
s . x = (Initialize s) . x by SCMFSA6C:3;
hence s . x = (Initialize s) . x ; :: thesis: verum

end;

then A3: s | NAT = (Initialize s) | NAT by A1, A2, FUNCT_1:165;
thus IExec I,s = (Result (s +* (Initialized I))) +* (s | NAT ) by SCMFSA6B:def 1
.= (Result ((Initialize s) +* (Initialized I))) +* (s | NAT ) by SCMFSA8A:8
.= IExec I,(Initialize s) by A3, SCMFSA6B:def 1 ; :: thesis: verum