let IL be non empty set ; :: thesis: for N being with_non-empty_elements set
for S being non empty stored-program steady-programmed AMI-Struct of IL,N
for i being Instruction of S
for s being State of S holds (Exec i,s) | IL = s | IL
let N be with_non-empty_elements set ; :: thesis: for S being non empty stored-program steady-programmed AMI-Struct of IL,N
for i being Instruction of S
for s being State of S holds (Exec i,s) | IL = s | IL
let S be non empty stored-program steady-programmed AMI-Struct of IL,N; :: thesis: for i being Instruction of S
for s being State of S holds (Exec i,s) | IL = s | IL
let i be Instruction of S; :: thesis: for s being State of S holds (Exec i,s) | IL = s | IL
let s be State of S; :: thesis: (Exec i,s) | IL = s | IL
A1: IL c= the carrier of S by Def3;
dom (Exec i,s) = the carrier of S by Th79;
then A2: dom ((Exec i,s) | IL) = IL by A1, RELAT_1:91;
dom s = the carrier of S by Th79;
then A3: dom (s | IL) = IL by A1, RELAT_1:91;
for x being set st x in IL holds
((Exec i,s) | IL) . x = (s | IL) . x

proof

let x be set ; :: thesis: ( x in IL implies ((Exec i,s) | IL) . x = (s | IL) . x )
assume x in IL ; :: thesis: ((Exec i,s) | IL) . x = (s | IL) . x
then reconsider l = x as Instruction-Location of S by Def4;
A4: l in IL by Def4;
hence ((Exec i,s) | IL) . x = (Exec i,s) . l by FUNCT_1:72
.= s . l by Def13
.= (s | IL) . x by A4, FUNCT_1:72 ;
:: thesis: verum

end;

hence (Exec i,s) | IL = s | IL by A2, A3, FUNCT_1:9; :: thesis: verum