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