let S be non empty 1-sorted ; :: thesis: for R being Ring

for d1 being Data-Location of R

for i1 being Nat holds [7,<*i1*>,<*d1*>] in SCM-Instr S

let R be Ring; :: thesis: for d1 being Data-Location of R

for i1 being Nat holds [7,<*i1*>,<*d1*>] in SCM-Instr S

let d1 be Data-Location of R; :: thesis: for i1 being Nat holds [7,<*i1*>,<*d1*>] in SCM-Instr S

let i1 be Nat; :: thesis: [7,<*i1*>,<*d1*>] in SCM-Instr S

reconsider d1 = d1 as Element of SCM-Data-Loc by Th1, AMI_3:27;

[7,<*i1*>,<*d1*>] in SCM-Instr S by SCMRINGI:11;

hence [7,<*i1*>,<*d1*>] in SCM-Instr S ; :: thesis: verum

for d1 being Data-Location of R

for i1 being Nat holds [7,<*i1*>,<*d1*>] in SCM-Instr S

let R be Ring; :: thesis: for d1 being Data-Location of R

for i1 being Nat holds [7,<*i1*>,<*d1*>] in SCM-Instr S

let d1 be Data-Location of R; :: thesis: for i1 being Nat holds [7,<*i1*>,<*d1*>] in SCM-Instr S

let i1 be Nat; :: thesis: [7,<*i1*>,<*d1*>] in SCM-Instr S

reconsider d1 = d1 as Element of SCM-Data-Loc by Th1, AMI_3:27;

[7,<*i1*>,<*d1*>] in SCM-Instr S by SCMRINGI:11;

hence [7,<*i1*>,<*d1*>] in SCM-Instr S ; :: thesis: verum