let p be Instruction-Sequence of SCM+FSA; :: thesis: for I being Program of SCM+FSA

for s being State of SCM+FSA holds IExec (I,p,s) = IExec (I,p,(Initialized s))

let I be Program of SCM+FSA; :: thesis: for s being State of SCM+FSA holds IExec (I,p,s) = IExec (I,p,(Initialized s))

let s be State of SCM+FSA; :: thesis: IExec (I,p,s) = IExec (I,p,(Initialized s))

set sp = s | NAT;

thus IExec (I,p,s) = Result ((p +* I),(Initialized (Initialized s))) by SCMFSA6B:def 1

.= IExec (I,p,(Initialized s)) by SCMFSA6B:def 1 ; :: thesis: verum

for s being State of SCM+FSA holds IExec (I,p,s) = IExec (I,p,(Initialized s))

let I be Program of SCM+FSA; :: thesis: for s being State of SCM+FSA holds IExec (I,p,s) = IExec (I,p,(Initialized s))

let s be State of SCM+FSA; :: thesis: IExec (I,p,s) = IExec (I,p,(Initialized s))

set sp = s | NAT;

thus IExec (I,p,s) = Result ((p +* I),(Initialized (Initialized s))) by SCMFSA6B:def 1

.= IExec (I,p,(Initialized s)) by SCMFSA6B:def 1 ; :: thesis: verum