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