let s be State of (Trivial-AMI IL,N); :: according to AMI_1:def 13 :: thesis: for i being Instruction of (Trivial-AMI IL,N)
for l being Instruction-Location of Trivial-AMI IL,N holds (Exec i,s) . l = s . l
let i be Instruction of (Trivial-AMI IL,N); :: thesis: for l being Instruction-Location of Trivial-AMI IL,N holds (Exec i,s) . l = s . l
let l be Instruction-Location of Trivial-AMI IL,N; :: thesis: (Exec i,s) . l = s . l
thus (Exec i,s) . l = s . l by Th9; :: thesis: verum