let s be State of SCM; :: according to AMI_1:def 13 :: thesis: for i being Instruction of SCM
for l being Element of NAT holds (Exec (i,s)) . l = s . l
let i be Instruction of SCM; :: thesis: for l being Element of NAT holds (Exec (i,s)) . l = s . l
let l be Element of NAT ; :: thesis: (Exec (i,s)) . l = s . l
thus (Exec (i,s)) . l = s . l by Lm14; :: thesis: verum