let I be Program of SCM+FSA; :: thesis: for s being State of SCM+FSA holds IExec (I,s) = IExec (I,(Initialized s))
let s be State of SCM+FSA; :: thesis: IExec (I,s) = IExec (I,(Initialized s))
set sp = s | NAT;
X: s +* (Initialized I) = (Initialized 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
.= (Result ((ProgramPart ((Initialized s) +* (Initialized I))),((Initialized s) +* (Initialized I)))) +* ((Initialized s) | NAT) by SCMFSA8C:36
.= IExec (I,(Initialized s)) by SCMFSA6B:def 1 ; :: thesis: verum