let a be Int-Location ; :: thesis: for f being FinSeq-Location holds (product" (AddressParts (InsCode (a :=len f)))) . 2 = SCM+FSA-Data*-Loc
let f be FinSeq-Location ; :: thesis: (product" (AddressParts (InsCode (a :=len f)))) . 2 = SCM+FSA-Data*-Loc
A1: InsCode (a :=len f) = 11 by SCMFSA_2:52;
dom (product" (AddressParts (InsCode (a :=len f)))) = {1,2} by Th41, SCMFSA_2:52;
then A2: 2 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)))) . 2

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