let s be State of SCM+FSA ; :: thesis: for I being Program of SCM+FSA holds IC (IExec I,s) = IC (Result (s +* (Initialized I)))
let I be Program of SCM+FSA ; :: thesis: IC (IExec I,s) = IC (Result (s +* (Initialized I)))
A1: dom s = ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) \/ NAT by SCMFSA6A:34;
A2: IExec I,s = (Result (s +* (Initialized I))) +* (s | NAT ) by SCMFSA6B:def 1;
A3: dom (s | NAT ) = (dom s) /\ NAT by RELAT_1:90
.= NAT by A1, XBOOLE_1:21 ;

now

assume IC SCM+FSA in dom (s | NAT ) ; :: thesis: contradiction
then reconsider l = IC SCM+FSA as Instruction-Location of SCM+FSA by A3, AMI_1:def 4;
l = IC SCM+FSA ;
hence contradiction by AMI_1:48; :: thesis: verum

end;

hence IC (IExec I,s) = IC (Result (s +* (Initialized I))) by A2, FUNCT_4:12; :: thesis: verum