let S be non empty 1-sorted ; :: thesis: for x being set

for R being Ring

for d1, d2 being Data-Location of R st x in {1,2,3,4} holds

[x,{},<*d1,d2*>] in SCM-Instr S

let x be set ; :: thesis: for R being Ring

for d1, d2 being Data-Location of R st x in {1,2,3,4} holds

[x,{},<*d1,d2*>] in SCM-Instr S

let R be Ring; :: thesis: for d1, d2 being Data-Location of R st x in {1,2,3,4} holds

[x,{},<*d1,d2*>] in SCM-Instr S

let d1, d2 be Data-Location of R; :: thesis: ( x in {1,2,3,4} implies [x,{},<*d1,d2*>] in SCM-Instr S )

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

( x in {1,2,3,4} implies [x,{},<*d1,d2*>] in SCM-Instr S ) by SCMRINGI:8;

hence ( x in {1,2,3,4} implies [x,{},<*d1,d2*>] in SCM-Instr S ) ; :: thesis: verum

for R being Ring

for d1, d2 being Data-Location of R st x in {1,2,3,4} holds

[x,{},<*d1,d2*>] in SCM-Instr S

let x be set ; :: thesis: for R being Ring

for d1, d2 being Data-Location of R st x in {1,2,3,4} holds

[x,{},<*d1,d2*>] in SCM-Instr S

let R be Ring; :: thesis: for d1, d2 being Data-Location of R st x in {1,2,3,4} holds

[x,{},<*d1,d2*>] in SCM-Instr S

let d1, d2 be Data-Location of R; :: thesis: ( x in {1,2,3,4} implies [x,{},<*d1,d2*>] in SCM-Instr S )

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

( x in {1,2,3,4} implies [x,{},<*d1,d2*>] in SCM-Instr S ) by SCMRINGI:8;

hence ( x in {1,2,3,4} implies [x,{},<*d1,d2*>] in SCM-Instr S ) ; :: thesis: verum