let R be good Ring; :: thesis: for loc being Instruction-Location of SCM R holds ObjectKind loc = SCM-Instr R
let loc be Instruction-Location of SCM R; :: thesis: ObjectKind loc = SCM-Instr R
reconsider i = loc as Element of NAT by AMI_1:def 4;
thus ObjectKind loc = (SCM-OK R) . i by SCMRING2:def 1
.= SCM-Instr R by SCMRING1:6 ; :: thesis: verum