let a be Int-Location ; :: thesis: for f being FinSeq-Location holds (product" (AddressParts (InsCode (a :=len f)))) . 1 = SCM+FSA-Data-Loc
let f be FinSeq-Location ; :: thesis: (product" (AddressParts (InsCode (a :=len f)))) . 1 = SCM+FSA-Data-Loc
dom (product" (AddressParts (InsCode (a :=len f)))) = {1,2} by Th41, SCMFSA_2:52;
then A1: 1 in dom (product" (AddressParts (InsCode (a :=len f)))) by TARSKI:def 2;

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

let x be set ; :: thesis: ( x in (product" (AddressParts (InsCode (a :=len f)))) . 1 implies x in SCM+FSA-Data-Loc )
assume x in (product" (AddressParts (InsCode (a :=len f)))) . 1 ; :: thesis: x in SCM+FSA-Data-Loc
then x in pi (AddressParts (InsCode (a :=len f))),1 by A1, CARD_3:93;
then consider g being Function such that
A2: g in AddressParts (InsCode (a :=len f)) and
A3: x = g . 1 by CARD_3:def 6;
consider I being Instruction of SCM+FSA such that
A4: g = AddressPart I and
A5: InsCode I = InsCode (a :=len f) by A2;
consider a being Int-Location , f being FinSeq-Location such that
A6: I = a :=len f by A5, SCMFSA_2:52, SCMFSA_2:64;
g = <*a,f*> by A4, A6, MCART_1:def 2;
then x = a by A3, FINSEQ_1:61;
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 (a :=len f)))) . 1 )
assume x in SCM+FSA-Data-Loc ; :: thesis: x in (product" (AddressParts (InsCode (a :=len f)))) . 1
then reconsider x = x as Int-Location by SCMFSA_2:28;
A7: <*x,f*> . 1 = x by FINSEQ_1:61;
InsCode (a :=len f) = 11 by SCMFSA_2:52;
then A8: InsCode (x :=len f) = InsCode (a :=len f) by SCMFSA_2:52;
AddressPart (x :=len f) = <*x,f*> by MCART_1:def 2;
then <*x,f*> in AddressParts (InsCode (a :=len f)) by A8;
then x in pi (AddressParts (InsCode (a :=len f))),1 by A7, CARD_3:def 6;
hence x in (product" (AddressParts (InsCode (a :=len f)))) . 1 by A1, CARD_3:93; :: thesis: verum