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