let R be good Ring; for a, b being Data-Location of R holds (product" (AddressParts (InsCode (AddTo a,b)))) . 1 = SCM-Data-Loc
let a, b be Data-Location of R; (product" (AddressParts (InsCode (AddTo a,b)))) . 1 = SCM-Data-Loc
dom (product" (AddressParts (InsCode (AddTo a,b)))) = {1,2}
by Th10, Th34;
then A1:
1 in dom (product" (AddressParts (InsCode (AddTo a,b))))
by TARSKI:def 2;
hereby TARSKI:def 3,
XBOOLE_0:def 10 SCM-Data-Loc c= (product" (AddressParts (InsCode (AddTo a,b)))) . 1
let x be
set ;
( x in (product" (AddressParts (InsCode (AddTo a,b)))) . 1 implies x in SCM-Data-Loc )assume
x in (product" (AddressParts (InsCode (AddTo a,b)))) . 1
;
x in SCM-Data-Loc then
x in pi (AddressParts (InsCode (AddTo a,b))),1
by A1, CARD_3:def 13;
then consider f being
Function such that A2:
f in AddressParts (InsCode (AddTo a,b))
and A3:
f . 1
= x
by CARD_3:def 6;
consider I being
Instruction of
(SCM R) such that A4:
f = AddressPart I
and A5:
InsCode I = InsCode (AddTo a,b)
by A2;
InsCode I = 2
by A5, MCART_1:def 1;
then consider d1,
d2 being
Data-Location of
R such that A6:
I = AddTo d1,
d2
by Th18;
x =
<*d1,d2*> . 1
by A3, A4, A6, MCART_1:def 2
.=
d1
by FINSEQ_1:61
;
hence
x in SCM-Data-Loc
by SCMRING2:1;
verum
end;
consider d1 being Data-Location of R;
let x be set ; TARSKI:def 3 ( not x in SCM-Data-Loc or x in (product" (AddressParts (InsCode (AddTo a,b)))) . 1 )
assume
x in SCM-Data-Loc
; x in (product" (AddressParts (InsCode (AddTo a,b)))) . 1
then reconsider x = x as Data-Location of R by SCMRING2:1;
( InsCode (AddTo a,b) = 2 & InsCode (AddTo x,d1) = 2 )
by MCART_1:def 1;
then
AddressPart (AddTo x,d1) in AddressParts (InsCode (AddTo a,b))
;
then A7:
(AddressPart (AddTo x,d1)) . 1 in pi (AddressParts (InsCode (AddTo a,b))),1
by CARD_3:def 6;
(AddressPart (AddTo x,d1)) . 1 =
<*x,d1*> . 1
by MCART_1:def 2
.=
x
by FINSEQ_1:61
;
hence
x in (product" (AddressParts (InsCode (AddTo a,b)))) . 1
by A1, A7, CARD_3:def 13; verum