let S be non empty 1-sorted ; :: thesis: for t being Element of S
for R being Ring
for d1 being Data-Location of R holds [5,{},<*d1,t*>] in SCM-Instr S
let t be Element of S; :: thesis: for R being Ring
for d1 being Data-Location of R holds [5,{},<*d1,t*>] in SCM-Instr S
let R be Ring; :: thesis: for d1 being Data-Location of R holds [5,{},<*d1,t*>] in SCM-Instr S
let d1 be Data-Location of R; :: thesis: [5,{},<*d1,t*>] in SCM-Instr S
reconsider d1 = d1 as Element of SCM-Data-Loc by Th1, AMI_3:27;
[5,{},<*d1,t*>] in SCM-Instr S by SCMRINGI:9;
hence [5,{},<*d1,t*>] in SCM-Instr S ; :: thesis: verum