let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated steady-programmed definite realistic Exec-preserving AMI-Struct of N
for s being State of S
for i being Instruction of S
for p being NAT -defined FinPartState of holds Exec i,(s +* p) = (Exec i,s) +* p
let S be non empty stored-program IC-Ins-separated steady-programmed definite realistic Exec-preserving AMI-Struct of N; :: thesis: for s being State of S
for i being Instruction of S
for p being NAT -defined FinPartState of holds Exec i,(s +* p) = (Exec i,s) +* p
let s be State of S; :: thesis: for i being Instruction of S
for p being NAT -defined FinPartState of holds Exec i,(s +* p) = (Exec i,s) +* p
let i be Instruction of S; :: thesis: for p being NAT -defined FinPartState of holds Exec i,(s +* p) = (Exec i,s) +* p
let p be NAT -defined FinPartState of ; :: thesis: Exec i,(s +* p) = (Exec i,s) +* p
set C = the carrier of S;
set I = NAT ;
set D = the carrier of S \ ({(IC S)} \/ NAT );
A1: dom p c= NAT by RELAT_1:def 18;
A2: dom s = the carrier of S by PARTFUN1:def 4;
A3: dom (s +* p) = the carrier of S by PARTFUN1:def 4;
A4: dom (Exec i,s) = the carrier of S by PARTFUN1:def 4;
A5: dom (Exec i,(s +* p)) = the carrier of S by PARTFUN1:def 4;
the carrier of S \ ({(IC S)} \/ NAT ) = (the carrier of S \ NAT ) \ {(IC S)} by XBOOLE_1:41;
then A6: (the carrier of S \ ({(IC S)} \/ NAT )) \/ {(IC S)} = (the carrier of S \ NAT ) \/ {(IC S)} by XBOOLE_1:39;
A7: {(IC S)} c= the carrier of S by ZFMISC_1:37;
{(IC S)} c= the carrier of S \ NAT

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {(IC S)} or x in the carrier of S \ NAT )
assume A8: x in {(IC S)} ; :: thesis: x in the carrier of S \ NAT
then A9: x = IC S by TARSKI:def 1;
not x in NAT by A9, AMI_1:48;
hence x in the carrier of S \ NAT by A7, A8, XBOOLE_0:def 5; :: thesis: verum

end;

then A10: the carrier of S \ NAT = (the carrier of S \ ({(IC S)} \/ NAT )) \/ {(IC S)} by A6, XBOOLE_1:12;
NAT c= the carrier of S \ {(IC S)} by Lm8;
then A11: the carrier of S = ({(IC S)} \/ (the carrier of S \ ({(IC S)} \/ NAT ))) \/ NAT by A7, Lm7;
(the carrier of S \ ({(IC S)} \/ NAT )) \/ {(IC S)} misses NAT

proof

assume not (the carrier of S \ ({(IC S)} \/ NAT )) \/ {(IC S)} misses NAT ; :: thesis: contradiction
then consider o being set such that
A12: o in (the carrier of S \ ({(IC S)} \/ NAT )) \/ {(IC S)} and
A13: o in NAT by XBOOLE_0:3;
reconsider l = o as Element of NAT by A13;
A14: ( o in the carrier of S \ ({(IC S)} \/ NAT ) or o in {(IC S)} ) by A12, XBOOLE_0:def 3;

per cases ( o in the carrier of S \ ({(IC S)} \/ NAT ) or o = IC S ) by A14, TARSKI:def 1;

suppose o in the carrier of S \ ({(IC S)} \/ NAT ) ; :: thesis: contradiction

then not o in {(IC S)} \/ NAT by XBOOLE_0:def 5;
hence contradiction by A13, XBOOLE_0:def 3; :: thesis: verum

end;

suppose o = IC S ; :: thesis: contradiction

then l = IC S ;
hence contradiction by AMI_1:48; :: thesis: verum

end;

end;

end;

then A15: (the carrier of S \ ({(IC S)} \/ NAT )) \/ {(IC S)} misses dom p by A1, XBOOLE_1:63;
then s | ((dom s) \ NAT ) = (s +* p) | ((dom (s +* p)) \ NAT ) by A2, A3, A10, FUNCT_4:76;
then s,s +* p equal_outside NAT by FUNCT_7:def 2;
then A16: Exec i,s, Exec i,(s +* p) equal_outside NAT by Def19;
A17: ((Exec i,s) +* p) | ((the carrier of S \ ({(IC S)} \/ NAT )) \/ {(IC S)}) = (Exec i,s) | ((the carrier of S \ ({(IC S)} \/ NAT )) \/ {(IC S)}) by A15, FUNCT_4:76
.= (Exec i,(s +* p)) | ((the carrier of S \ ({(IC S)} \/ NAT )) \/ {(IC S)}) by A4, A5, A10, A16, FUNCT_7:def 2 ;
A18: (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)) | (({(IC S)} \/ (the carrier of S \ ({(IC S)} \/ NAT ))) \/ NAT ) by A5, A11, RELAT_1:98
.= (((Exec i,s) +* p) | ({(IC S)} \/ (the carrier of S \ ({(IC S)} \/ NAT )))) +* (((Exec i,s) +* p) | NAT ) by A17, A18, FUNCT_4:83
.= ((Exec i,s) +* p) | (({(IC S)} \/ (the carrier of S \ ({(IC S)} \/ NAT ))) \/ NAT ) by FUNCT_4:83
.= ((Exec i,s) +* p) | (dom ((Exec i,s) +* p)) by A11, PARTFUN1:def 4
.= (Exec i,s) +* p by RELAT_1:98 ; :: thesis: verum