let R be good Ring; :: thesis: for r being Element of R
for a being Data-Location of R holds (product" (AddressParts (InsCode (a := r)))) . 2 = the carrier of R
let r be Element of R; :: thesis: for a being Data-Location of R holds (product" (AddressParts (InsCode (a := r)))) . 2 = the carrier of R
let a be Data-Location of R; :: thesis: (product" (AddressParts (InsCode (a := r)))) . 2 = the carrier of R
A1: InsCode (a := r) = 5 by MCART_1:def 1;
dom (product" (AddressParts (InsCode (a := r)))) = {1,2} by Th13, Th37;
then A2: 2 in dom (product" (AddressParts (InsCode (a := r)))) by TARSKI:def 2;
thus (product" (AddressParts (InsCode (a := r)))) . 2 c= the carrier of R :: according to XBOOLE_0:def 10 :: thesis: the carrier of R c= (product" (AddressParts (InsCode (a := r)))) . 2

proof

let k be set ; :: according to TARSKI:def 3 :: thesis: ( not k in (product" (AddressParts (InsCode (a := r)))) . 2 or k in the carrier of R )
assume k in (product" (AddressParts (InsCode (a := r)))) . 2 ; :: thesis: k in the carrier of R
then k in pi (AddressParts (InsCode (a := r))),2 by A2, CARD_3:def 13;
then consider g being Function such that
A3: g in AddressParts (InsCode (a := r)) and
A4: g . 2 = k by CARD_3:def 6;
consider I being Instruction of (SCM R) such that
A5: g = AddressPart I and
A6: InsCode I = InsCode (a := r) by A3;
InsCode I = 5 by A6, MCART_1:def 1;
then consider d1 being Data-Location of R, r1 being Element of R such that
A7: I = d1 := r1 by Th21;
k = <*d1,r1*> . 2 by A4, A5, A7, MCART_1:def 2
.= r1 by FINSEQ_1:61 ;
hence k in the carrier of R ; :: thesis: verum

end;

let k be set ; :: according to TARSKI:def 3 :: thesis: ( not k in the carrier of R or k in (product" (AddressParts (InsCode (a := r)))) . 2 )
assume k in the carrier of R ; :: thesis: k in (product" (AddressParts (InsCode (a := r)))) . 2
then reconsider r1 = k as Element of R ;
consider b being Data-Location of R;
set J = b := r1;
A8: AddressPart (b := r1) = <*b,r1*> by MCART_1:def 2;
InsCode (b := r1) = 5 by MCART_1:def 1;
then AddressPart (b := r1) in AddressParts (InsCode (a := r)) by A1;
then A9: (AddressPart (b := r1)) . 2 in pi (AddressParts (InsCode (a := r))),2 by CARD_3:def 6;
r1 = <*b,r1*> . 2 by FINSEQ_1:61;
hence k in (product" (AddressParts (InsCode (a := r)))) . 2 by A2, A8, A9, CARD_3:def 13; :: thesis: verum