let i be Instruction of SCMPDS ; :: thesis: for s being State of SCMPDS
for p being preProgram of SCMPDS holds Exec i,(s +* p) = (Exec i,s) +* p
let s be State of SCMPDS ; :: thesis: for p being preProgram of SCMPDS holds Exec i,(s +* p) = (Exec i,s) +* p
let p be preProgram of SCMPDS ; :: thesis: Exec i,(s +* p) = (Exec i,s) +* p
A1: dom p c= NAT by RELAT_1:def 18;

now

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

end;

then SCM-Data-Loc \/ {(IC SCMPDS )} misses NAT by AMI_2:29, XBOOLE_1:70;
then A4: SCM-Data-Loc \/ {(IC SCMPDS )} misses dom p by A1, XBOOLE_1:63;
then A5: s | (SCM-Data-Loc \/ {(IC SCMPDS )}) = (s +* p) | (SCM-Data-Loc \/ {(IC SCMPDS )}) by FUNCT_4:76;
A6: ((Exec i,s) +* p) | (SCM-Data-Loc \/ {(IC SCMPDS )}) = (Exec i,s) | (SCM-Data-Loc \/ {(IC SCMPDS )}) by A4, FUNCT_4:76
.= (Exec i,(s +* p)) | (SCM-Data-Loc \/ {(IC SCMPDS )}) by A5, Th7 ;
A7: (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)) | ((SCM-Data-Loc \/ {(IC SCMPDS )}) \/ NAT ) by AMI_1:79, AMI_3:4
.= (((Exec i,s) +* p) | (SCM-Data-Loc \/ {(IC SCMPDS )})) +* (((Exec i,s) +* p) | NAT ) by A6, A7, FUNCT_4:83
.= ((Exec i,s) +* p) | the carrier of SCMPDS by AMI_3:4, FUNCT_4:83
.= ((Exec i,s) +* p) | (dom ((Exec i,s) +* p)) by AMI_1:79
.= (Exec i,s) +* p by RELAT_1:97 ; :: thesis: verum