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: now

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

end;

Int-Locations \/ FinSeq-Locations misses NAT by SCMFSA_2:13, SCMFSA_2:14, XBOOLE_1:70;
then ( dom p c= NAT & (Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )} misses NAT ) by A1, RELAT_1:def 18, XBOOLE_1:70;
then A4: (Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )} misses dom p by XBOOLE_1:63;
then A5: s | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) = (s +* p) | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) by FUNCT_4:76;
A6: ((Exec i,s) +* p) | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) = (Exec i,s) | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) by A4, FUNCT_4:76
.= (Exec i,(s +* p)) | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) by A5, Th4 ;
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)) | (((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) \/ NAT ) by PARTFUN1:def 4, SCMFSA_2:8
.= (((Exec i,s) +* p) | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )})) +* (((Exec i,s) +* p) | NAT ) by A6, A7, 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 PARTFUN1:def 4
.= (Exec i,s) +* p by RELAT_1:97 ; :: thesis: verum