let a, b be Int-Location ; :: thesis:
let f be FinSeq-Location ; :: thesis:
A1: InsCode (f,a := b) = 10 by SCMFSA_2:51;
dom (product" (AddressParts (InsCode (f,a := b)))) = {1,2,3} by Th40, SCMFSA_2:51;
then A2: 2 in dom (product" (AddressParts (InsCode (f,a := b)))) by ENUMSET1:def 1;

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis:

let x be set ; :: thesis:
assume x in (product" (AddressParts (InsCode (f,a := b)))) . 2 ; :: thesis:
then x in pi (AddressParts (InsCode (f,a := b))),2 by A2, CARD_3:93;
then consider g being Function such that
A3: g in AddressParts (InsCode (f,a := b)) and
A4: x = g . 2 by CARD_3:def 6;
consider I being Instruction of SCM+FSA such that
A5: g = AddressPart I and
A6: InsCode I = InsCode (f,a := b) by A3;
consider a, b being Int-Location , f being FinSeq-Location such that
A7: I = f,a := b by A1, A6, SCMFSA_2:63;
g = <*b,f,a*> by A5, A7, MCART_1:def 2;
then x = f by A4, FINSEQ_1:62;
hence x in SCM+FSA-Data*-Loc by SCMFSA_2:def 5; :: thesis:

end;

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in SCM+FSA-Data*-Loc ; :: thesis:
then reconsider x = x as FinSeq-Location by SCMFSA_2:29;
A8: AddressPart (x,a := b) = <*b,x,a*> by MCART_1:def 2;
InsCode (f,a := b) = InsCode (x,a := b) by A1, SCMFSA_2:51;
then A9: <*b,x,a*> in AddressParts (InsCode (f,a := b)) by A8;
<*b,x,a*> . 2 = x by FINSEQ_1:62;
then x in pi (AddressParts (InsCode (f,a := b))),2 by A9, CARD_3:def 6;
hence x in (product" (AddressParts (InsCode (f,a := b)))) . 2 by A2, CARD_3:93; :: thesis: