let S be non empty 1-sorted ; :: thesis: for t being Element of S
for R being good 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 good Ring
for d1 being Data-Location of R holds [5,{} ,<*d1,t*>] in SCM-Instr S
let R be good 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;
[5,{} ,<*D1,t*>] in { [5,{} ,<*i,a*>] where i is Element of SCM-Data-Loc , a is Element of S : verum } ;
hence [5,{} ,<*d1,t*>] in SCM-Instr S by XBOOLE_0:def 3; :: thesis: verum