let i be Instruction of SCM+FSA ; :: thesis: for s being State of SCM+FSA
for p being preProgram of SCM+FSA holds Exec i,(s +* p) = (Exec i,s) +* p
let s be State of SCM+FSA ; :: thesis: for p being preProgram of SCM+FSA holds Exec i,(s +* p) = (Exec i,s) +* p
let p be preProgram of SCM+FSA ; :: thesis: Exec i,(s +* p) = (Exec i,s) +* p
A1: dom p c= NAT by RELAT_1:def 18;
A2: Int-Locations \/ FinSeq-Locations misses NAT by SCMFSA_2:13, SCMFSA_2:14, XBOOLE_1:70;

now

assume {(IC SCM+FSA )} meets NAT ; :: thesis: contradiction
then consider x being set such that
A3: x in {(IC SCM+FSA )} and
A4: x in NAT by XBOOLE_0:3;
reconsider l = x as Instruction-Location of SCM+FSA by A4, AMI_1:def 4;
l = IC SCM+FSA by A3, TARSKI:def 1;
hence contradiction by AMI_1:48; :: thesis: verum

end;

then (Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )} misses NAT by A2, XBOOLE_1:70;
then A5: (Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )} misses dom p by A1, XBOOLE_1:63;
then A6: s | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) = (s +* p) | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) by FUNCT_4:76;
A7: ((Exec i,s) +* p) | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) = (Exec i,s) | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) by A5, FUNCT_4:76
.= (Exec i,(s +* p)) | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) by A6, Th4 ;
A8: (Exec i,(s +* p)) | NAT = (s +* p) | NAT by AMI_1:117
.= (s | NAT ) +* (p | NAT ) by FUNCT_4:75
.= ((Exec i,s) | NAT ) +* (p | NAT ) by AMI_1:117
.= ((Exec i,s) +* p) | NAT by FUNCT_4:75 ;
thus Exec i,(s +* p) = (Exec i,(s +* p)) | (dom (Exec i,(s +* p))) by RELAT_1:97
.= (Exec i,(s +* p)) | (((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) \/ NAT ) by AMI_1:79, SCMFSA_2:8
.= (((Exec i,s) +* p) | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )})) +* (((Exec i,s) +* p) | NAT ) by A7, A8, FUNCT_4:83
.= ((Exec i,s) +* p) | the carrier of SCM+FSA by FUNCT_4:83, SCMFSA_2:8
.= ((Exec i,s) +* p) | (dom ((Exec i,s) +* p)) by AMI_1:79
.= (Exec i,s) +* p by RELAT_1:97 ; :: thesis: verum