let N be with_non-empty_elements set ; :: thesis: for A being non empty stored-program IC-Ins-separated steady-programmed definite standard AMI-Struct of N
for I being Instruction of
for s being State of
for o being Object of
for w being Element of ObjectKind o
for i being Instruction-Location of A holds (Exec I,(s +* o,w)) . i = ((Exec I,s) +* o,w) . i
let A be non empty stored-program IC-Ins-separated steady-programmed definite standard AMI-Struct of N; :: thesis: for I being Instruction of
for s being State of
for o being Object of
for w being Element of ObjectKind o
for i being Instruction-Location of A holds (Exec I,(s +* o,w)) . i = ((Exec I,s) +* o,w) . i
let I be Instruction of ; :: thesis: for s being State of
for o being Object of
for w being Element of ObjectKind o
for i being Instruction-Location of A holds (Exec I,(s +* o,w)) . i = ((Exec I,s) +* o,w) . i
let s be State of ; :: thesis: for o being Object of
for w being Element of ObjectKind o
for i being Instruction-Location of A holds (Exec I,(s +* o,w)) . i = ((Exec I,s) +* o,w) . i
let o be Object of ; :: thesis: for w being Element of ObjectKind o
for i being Instruction-Location of A holds (Exec I,(s +* o,w)) . i = ((Exec I,s) +* o,w) . i
let w be Element of ObjectKind o; :: thesis: for i being Instruction-Location of A holds (Exec I,(s +* o,w)) . i = ((Exec I,s) +* o,w) . i
let i be Instruction-Location of A; :: thesis: (Exec I,(s +* o,w)) . i = ((Exec I,s) +* o,w) . i
A1: (Exec I,(s +* o,w)) . i = (s +* o,w) . i by AMI_1:def 13;
A2: dom (Exec I,s) = the carrier of A by AMI_1:79;
A3: dom s = the carrier of A by AMI_1:79;

per cases ( i = o or i <> o ) ;

suppose A4: i = o ; :: thesis: (Exec I,(s +* o,w)) . i = ((Exec I,s) +* o,w) . i

hence (Exec I,(s +* o,w)) . i = w by A1, A3, FUNCT_7:33
.= ((Exec I,s) +* o,w) . i by A2, A4, FUNCT_7:33 ;
:: thesis: verum

end;

suppose A5: i <> o ; :: thesis: (Exec I,(s +* o,w)) . i = ((Exec I,s) +* o,w) . i

hence (Exec I,(s +* o,w)) . i = s . i by A1, FUNCT_7:34
.= (Exec I,s) . i by AMI_1:def 13
.= ((Exec I,s) +* o,w) . i by A5, FUNCT_7:34 ;
:: thesis: verum

end;

end;