let b, a be Int-Location ; :: thesis: for f being FinSeq-Location holds (product" (AddressParts (InsCode (b := f,a)))) . 3 = SCM+FSA-Data-Loc
let f be FinSeq-Location ; :: thesis: (product" (AddressParts (InsCode (b := f,a)))) . 3 = SCM+FSA-Data-Loc
A1: InsCode (b := f,a) = 9 by SCMFSA_2:50;
dom (product" (AddressParts (InsCode (b := f,a)))) = {1,2,3} by Th39, SCMFSA_2:50;
then A2: 3 in dom (product" (AddressParts (InsCode (b := f,a)))) by ENUMSET1:def 1;

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: SCM+FSA-Data-Loc c= (product" (AddressParts (InsCode (b := f,a)))) . 3

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

end;

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