let s be State of SCM+FSA ; :: thesis: for I being Program of SCM+FSA holds IExec I,s = IExec I,(Initialized s)
set A = NAT ;
set D = Int-Locations \/ FinSeq-Locations ;
let I be Program of SCM+FSA ; :: thesis: IExec I,s = IExec I,(Initialized s)
A1: for x being set st x in NAT holds
s . x = (Initialized s) . x by SCMFSA6C:3;
dom (Initialized s) = ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) \/ NAT by SCMFSA6A:34;
then A2: NAT c= dom (Initialized s) by XBOOLE_1:7;
dom s = ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) \/ NAT by SCMFSA6A:34;
then NAT c= dom s by XBOOLE_1:7;
then A3: s | NAT = (Initialized s) | NAT by A2, A1, FUNCT_1:165;
X: (Initialized s) +* (Initialized I) = s +* (Initialized I) by SCMFSA8A:8;
thus IExec I,s = (Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (s | NAT ) by SCMFSA6B:def 1
.= (Result (ProgramPart ((Initialized s) +* (Initialized I))),((Initialized s) +* (Initialized I))) +* (s | NAT ) by X
.= IExec I,(Initialized s) by A3, SCMFSA6B:def 1 ; :: thesis: verum