let T be InsType of SCM+FSA ; :: according to AMISTD_2:def 11 :: thesis:

per cases by Lm4;

reconsider f = {} as Function ;
take f ; :: according to CARD_3:def 14 :: thesis:
thus AddressParts T = product f by A1, Th30, CARD_3:19; :: thesis:

end;

suppose A2: T = 1 ; :: thesis:

take product" (AddressParts T) ; :: according to CARD_3:def 14 :: thesis:
thus AddressParts T c= product (product" (AddressParts T)) by CARD_3:94; :: according to XBOOLE_0:def 10 :: thesis:
let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in product (product" (AddressParts T)) ; :: thesis:
then consider f being Function such that
A3: x = f and
A4: dom f = dom (product" (AddressParts T)) and
A5: for k being set st k in dom (product" (AddressParts T)) holds
f . k in (product" (AddressParts T)) . k by CARD_3:def 5;
A6: dom (product" (AddressParts T)) = {1,2} by A2, Th31;
then A7: 1 in dom (product" (AddressParts T)) by TARSKI:def 2;
then f . 1 in (product" (AddressParts T)) . 1 by A5;
then f . 1 in pi (AddressParts T),1 by A7, CARD_3:def 13;
then consider g being Function such that
A8: g in AddressParts T and
A9: g . 1 = f . 1 by CARD_3:def 6;
A10: 2 in dom (product" (AddressParts T)) by A6, TARSKI:def 2;
then f . 2 in (product" (AddressParts T)) . 2 by A5;
then f . 2 in pi (AddressParts T),2 by A10, CARD_3:def 13;
then consider h being Function such that
A11: h in AddressParts T and
A12: h . 2 = f . 2 by CARD_3:def 6;
consider I being Instruction of SCM+FSA such that
A13: g = AddressPart I and
A14: InsCode I = T by A8;
consider d1, b being Int-Location such that
A15: I = d1 := b by A2, A14, SCMFSA_2:54;
A16: g = <*d1,b*> by A13, A15, Th18;
consider J being Instruction of SCM+FSA such that
A17: h = AddressPart J and
A18: InsCode J = T by A11;
consider a, d2 being Int-Location such that
A19: J = a := d2 by A2, A18, SCMFSA_2:54;
A20: h = <*a,d2*> by A17, A19, Th18;
A21: dom <*d1,d2*> = {1,2} by FINSEQ_1:4, FINSEQ_3:29;
for k being set st k in {1,2} holds
<*d1,d2*> . k = f . k

proof

let k be set ; :: thesis:
assume A22: k in {1,2} ; :: thesis:

per cases by A22, TARSKI:def 2;

suppose A23: k = 1 ; :: thesis:

<*d1,d2*> . 1 = d1 by FINSEQ_1:61
.= f . 1 by A9, A16, FINSEQ_1:61 ;
hence <*d1,d2*> . k = f . k by A23; :: thesis:

end;

suppose A24: k = 2 ; :: thesis:

<*d1,d2*> . 2 = d2 by FINSEQ_1:61
.= f . 2 by A12, A20, FINSEQ_1:61 ;
hence <*d1,d2*> . k = f . k by A24; :: thesis:

end;

then A25: <*d1,d2*> = f by A4, A6, A21, FUNCT_1:9;
( InsCode (d1 := d2) = 1 & AddressPart (d1 := d2) = <*d1,d2*> ) by Th18, SCMFSA_2:42;
hence x in AddressParts T by A2, A3, A25; :: thesis:

end;

suppose A26: T = 2 ; :: thesis:

take product" (AddressParts T) ; :: according to CARD_3:def 14 :: thesis:
thus AddressParts T c= product (product" (AddressParts T)) by CARD_3:94; :: according to XBOOLE_0:def 10 :: thesis:
let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in product (product" (AddressParts T)) ; :: thesis:
then consider f being Function such that
A27: x = f and
A28: dom f = dom (product" (AddressParts T)) and
A29: for k being set st k in dom (product" (AddressParts T)) holds
f . k in (product" (AddressParts T)) . k by CARD_3:def 5;
A30: dom (product" (AddressParts T)) = {1,2} by A26, Th32;
then A31: 1 in dom (product" (AddressParts T)) by TARSKI:def 2;
then f . 1 in (product" (AddressParts T)) . 1 by A29;
then f . 1 in pi (AddressParts T),1 by A31, CARD_3:def 13;
then consider g being Function such that
A32: g in AddressParts T and
A33: g . 1 = f . 1 by CARD_3:def 6;
A34: 2 in dom (product" (AddressParts T)) by A30, TARSKI:def 2;
then f . 2 in (product" (AddressParts T)) . 2 by A29;
then f . 2 in pi (AddressParts T),2 by A34, CARD_3:def 13;
then consider h being Function such that
A35: h in AddressParts T and
A36: h . 2 = f . 2 by CARD_3:def 6;
consider I being Instruction of SCM+FSA such that
A37: g = AddressPart I and
A38: InsCode I = T by A32;
consider d1, b being Int-Location such that
A39: I = AddTo d1,b by A26, A38, SCMFSA_2:55;
A40: g = <*d1,b*> by A37, A39, Th19;
consider J being Instruction of SCM+FSA such that
A41: h = AddressPart J and
A42: InsCode J = T by A35;
consider a, d2 being Int-Location such that
A43: J = AddTo a,d2 by A26, A42, SCMFSA_2:55;
A44: h = <*a,d2*> by A41, A43, Th19;
A45: dom <*d1,d2*> = {1,2} by FINSEQ_1:4, FINSEQ_3:29;
for k being set st k in {1,2} holds
<*d1,d2*> . k = f . k

proof

let k be set ; :: thesis:
assume A46: k in {1,2} ; :: thesis:

per cases by A46, TARSKI:def 2;

suppose A47: k = 1 ; :: thesis:

<*d1,d2*> . 1 = d1 by FINSEQ_1:61
.= f . 1 by A33, A40, FINSEQ_1:61 ;
hence <*d1,d2*> . k = f . k by A47; :: thesis:

end;

suppose A48: k = 2 ; :: thesis:

<*d1,d2*> . 2 = d2 by FINSEQ_1:61
.= f . 2 by A36, A44, FINSEQ_1:61 ;
hence <*d1,d2*> . k = f . k by A48; :: thesis:

end;

then A49: <*d1,d2*> = f by A28, A30, A45, FUNCT_1:9;
( InsCode (AddTo d1,d2) = 2 & AddressPart (AddTo d1,d2) = <*d1,d2*> ) by Th19, SCMFSA_2:43;
hence x in AddressParts T by A26, A27, A49; :: thesis:

end;

suppose A50: T = 3 ; :: thesis:

take product" (AddressParts T) ; :: according to CARD_3:def 14 :: thesis:
thus AddressParts T c= product (product" (AddressParts T)) by CARD_3:94; :: according to XBOOLE_0:def 10 :: thesis:
let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in product (product" (AddressParts T)) ; :: thesis:
then consider f being Function such that
A51: x = f and
A52: dom f = dom (product" (AddressParts T)) and
A53: for k being set st k in dom (product" (AddressParts T)) holds
f . k in (product" (AddressParts T)) . k by CARD_3:def 5;
A54: dom (product" (AddressParts T)) = {1,2} by A50, Th33;
then A55: 1 in dom (product" (AddressParts T)) by TARSKI:def 2;
then f . 1 in (product" (AddressParts T)) . 1 by A53;
then f . 1 in pi (AddressParts T),1 by A55, CARD_3:def 13;
then consider g being Function such that
A56: g in AddressParts T and
A57: g . 1 = f . 1 by CARD_3:def 6;
A58: 2 in dom (product" (AddressParts T)) by A54, TARSKI:def 2;
then f . 2 in (product" (AddressParts T)) . 2 by A53;
then f . 2 in pi (AddressParts T),2 by A58, CARD_3:def 13;
then consider h being Function such that
A59: h in AddressParts T and
A60: h . 2 = f . 2 by CARD_3:def 6;
consider I being Instruction of SCM+FSA such that
A61: g = AddressPart I and
A62: InsCode I = T by A56;
consider d1, b being Int-Location such that
A63: I = SubFrom d1,b by A50, A62, SCMFSA_2:56;
A64: g = <*d1,b*> by A61, A63, Th20;
consider J being Instruction of SCM+FSA such that
A65: h = AddressPart J and
A66: InsCode J = T by A59;
consider a, d2 being Int-Location such that
A67: J = SubFrom a,d2 by A50, A66, SCMFSA_2:56;
A68: h = <*a,d2*> by A65, A67, Th20;
A69: dom <*d1,d2*> = {1,2} by FINSEQ_1:4, FINSEQ_3:29;
for k being set st k in {1,2} holds
<*d1,d2*> . k = f . k

proof

let k be set ; :: thesis:
assume A70: k in {1,2} ; :: thesis:

per cases by A70, TARSKI:def 2;

suppose A71: k = 1 ; :: thesis:

<*d1,d2*> . 1 = d1 by FINSEQ_1:61
.= f . 1 by A57, A64, FINSEQ_1:61 ;
hence <*d1,d2*> . k = f . k by A71; :: thesis:

end;

suppose A72: k = 2 ; :: thesis:

<*d1,d2*> . 2 = d2 by FINSEQ_1:61
.= f . 2 by A60, A68, FINSEQ_1:61 ;
hence <*d1,d2*> . k = f . k by A72; :: thesis:

end;

then A73: <*d1,d2*> = f by A52, A54, A69, FUNCT_1:9;
( InsCode (SubFrom d1,d2) = 3 & AddressPart (SubFrom d1,d2) = <*d1,d2*> ) by Th20, SCMFSA_2:44;
hence x in AddressParts T by A50, A51, A73; :: thesis:

end;

suppose A74: T = 4 ; :: thesis:

take product" (AddressParts T) ; :: according to CARD_3:def 14 :: thesis:
thus AddressParts T c= product (product" (AddressParts T)) by CARD_3:94; :: according to XBOOLE_0:def 10 :: thesis:
let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in product (product" (AddressParts T)) ; :: thesis:
then consider f being Function such that
A75: x = f and
A76: dom f = dom (product" (AddressParts T)) and
A77: for k being set st k in dom (product" (AddressParts T)) holds
f . k in (product" (AddressParts T)) . k by CARD_3:def 5;
A78: dom (product" (AddressParts T)) = {1,2} by A74, Th34;
then A79: 1 in dom (product" (AddressParts T)) by TARSKI:def 2;
then f . 1 in (product" (AddressParts T)) . 1 by A77;
then f . 1 in pi (AddressParts T),1 by A79, CARD_3:def 13;
then consider g being Function such that
A80: g in AddressParts T and
A81: g . 1 = f . 1 by CARD_3:def 6;
A82: 2 in dom (product" (AddressParts T)) by A78, TARSKI:def 2;
then f . 2 in (product" (AddressParts T)) . 2 by A77;
then f . 2 in pi (AddressParts T),2 by A82, CARD_3:def 13;
then consider h being Function such that
A83: h in AddressParts T and
A84: h . 2 = f . 2 by CARD_3:def 6;
consider I being Instruction of SCM+FSA such that
A85: g = AddressPart I and
A86: InsCode I = T by A80;
consider d1, b being Int-Location such that
A87: I = MultBy d1,b by A74, A86, SCMFSA_2:57;
A88: g = <*d1,b*> by A85, A87, Th21;
consider J being Instruction of SCM+FSA such that
A89: h = AddressPart J and
A90: InsCode J = T by A83;
consider a, d2 being Int-Location such that
A91: J = MultBy a,d2 by A74, A90, SCMFSA_2:57;
A92: h = <*a,d2*> by A89, A91, Th21;
A93: dom <*d1,d2*> = {1,2} by FINSEQ_1:4, FINSEQ_3:29;
for k being set st k in {1,2} holds
<*d1,d2*> . k = f . k

proof

let k be set ; :: thesis:
assume A94: k in {1,2} ; :: thesis:

per cases by A94, TARSKI:def 2;

suppose A95: k = 1 ; :: thesis:

<*d1,d2*> . 1 = d1 by FINSEQ_1:61
.= f . 1 by A81, A88, FINSEQ_1:61 ;
hence <*d1,d2*> . k = f . k by A95; :: thesis:

end;

suppose A96: k = 2 ; :: thesis:

<*d1,d2*> . 2 = d2 by FINSEQ_1:61
.= f . 2 by A84, A92, FINSEQ_1:61 ;
hence <*d1,d2*> . k = f . k by A96; :: thesis:

end;

then A97: <*d1,d2*> = f by A76, A78, A93, FUNCT_1:9;
( InsCode (MultBy d1,d2) = 4 & AddressPart (MultBy d1,d2) = <*d1,d2*> ) by Th21, SCMFSA_2:45;
hence x in AddressParts T by A74, A75, A97; :: thesis:

end;

suppose A98: T = 5 ; :: thesis:

take product" (AddressParts T) ; :: according to CARD_3:def 14 :: thesis:
thus AddressParts T c= product (product" (AddressParts T)) by CARD_3:94; :: according to XBOOLE_0:def 10 :: thesis:
let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in product (product" (AddressParts T)) ; :: thesis:
then consider f being Function such that
A99: x = f and
A100: dom f = dom (product" (AddressParts T)) and
A101: for k being set st k in dom (product" (AddressParts T)) holds
f . k in (product" (AddressParts T)) . k by CARD_3:def 5;
A102: dom (product" (AddressParts T)) = {1,2} by A98, Th35;
then A103: 1 in dom (product" (AddressParts T)) by TARSKI:def 2;
then f . 1 in (product" (AddressParts T)) . 1 by A101;
then f . 1 in pi (AddressParts T),1 by A103, CARD_3:def 13;
then consider g being Function such that
A104: g in AddressParts T and
A105: g . 1 = f . 1 by CARD_3:def 6;
A106: 2 in dom (product" (AddressParts T)) by A102, TARSKI:def 2;
then f . 2 in (product" (AddressParts T)) . 2 by A101;
then f . 2 in pi (AddressParts T),2 by A106, CARD_3:def 13;
then consider h being Function such that
A107: h in AddressParts T and
A108: h . 2 = f . 2 by CARD_3:def 6;
consider I being Instruction of SCM+FSA such that
A109: g = AddressPart I and
A110: InsCode I = T by A104;
consider d1, b being Int-Location such that
A111: I = Divide d1,b by A98, A110, SCMFSA_2:58;
A112: g = <*d1,b*> by A109, A111, Th22;
consider J being Instruction of SCM+FSA such that
A113: h = AddressPart J and
A114: InsCode J = T by A107;
consider a, d2 being Int-Location such that
A115: J = Divide a,d2 by A98, A114, SCMFSA_2:58;
A116: h = <*a,d2*> by A113, A115, Th22;
A117: dom <*d1,d2*> = {1,2} by FINSEQ_1:4, FINSEQ_3:29;
for k being set st k in {1,2} holds
<*d1,d2*> . k = f . k

proof

let k be set ; :: thesis:
assume A118: k in {1,2} ; :: thesis:

per cases by A118, TARSKI:def 2;

suppose A119: k = 1 ; :: thesis:

<*d1,d2*> . 1 = d1 by FINSEQ_1:61
.= f . 1 by A105, A112, FINSEQ_1:61 ;
hence <*d1,d2*> . k = f . k by A119; :: thesis:

end;

suppose A120: k = 2 ; :: thesis:

<*d1,d2*> . 2 = d2 by FINSEQ_1:61
.= f . 2 by A108, A116, FINSEQ_1:61 ;
hence <*d1,d2*> . k = f . k by A120; :: thesis:

end;

then A121: <*d1,d2*> = f by A100, A102, A117, FUNCT_1:9;
( InsCode (Divide d1,d2) = 5 & AddressPart (Divide d1,d2) = <*d1,d2*> ) by Th22, SCMFSA_2:46;
hence x in AddressParts T by A98, A99, A121; :: thesis:

end;

suppose A122: T = 6 ; :: thesis:

proof

let k be set ; :: thesis:
assume k in {1} ; :: thesis:
then k = 1 by TARSKI:def 1;
hence <*i1*> . k = f . k by A129, A130, A132, Th23; :: thesis:

end;

then A134: <*i1*> = f by A124, A126, A133, FUNCT_1:9;
( InsCode (goto i1) = 6 & AddressPart (goto i1) = <*i1*> ) by Th23, SCMFSA_2:47;
hence x in AddressParts T by A122, A123, A134; :: thesis:

end;

suppose A135: T = 7 ; :: thesis:

take product" (AddressParts T) ; :: according to CARD_3:def 14 :: thesis:
thus AddressParts T c= product (product" (AddressParts T)) by CARD_3:94; :: according to XBOOLE_0:def 10 :: thesis:
let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in product (product" (AddressParts T)) ; :: thesis:
then consider f being Function such that
A136: x = f and
A137: dom f = dom (product" (AddressParts T)) and
A138: for k being set st k in dom (product" (AddressParts T)) holds
f . k in (product" (AddressParts T)) . k by CARD_3:def 5;
A139: dom (product" (AddressParts T)) = {1,2} by A135, Th37;
then A140: 1 in dom (product" (AddressParts T)) by TARSKI:def 2;
then f . 1 in (product" (AddressParts T)) . 1 by A138;
then f . 1 in pi (AddressParts T),1 by A140, CARD_3:def 13;
then consider g being Function such that
A141: g in AddressParts T and
A142: g . 1 = f . 1 by CARD_3:def 6;
A143: 2 in dom (product" (AddressParts T)) by A139, TARSKI:def 2;
then f . 2 in (product" (AddressParts T)) . 2 by A138;
then f . 2 in pi (AddressParts T),2 by A143, CARD_3:def 13;
then consider h being Function such that
A144: h in AddressParts T and
A145: h . 2 = f . 2 by CARD_3:def 6;
consider I being Instruction of SCM+FSA such that
A146: g = AddressPart I and
A147: InsCode I = T by A141;
consider i1 being Instruction-Location of SCM+FSA , d1 being Int-Location such that
A148: I = d1 =0_goto i1 by A135, A147, SCMFSA_2:60;
A149: g = <*i1,d1*> by A146, A148, Th24;
consider J being Instruction of SCM+FSA such that
A150: h = AddressPart J and
A151: InsCode J = T by A144;
consider i2 being Instruction-Location of SCM+FSA , d2 being Int-Location such that
A152: J = d2 =0_goto i2 by A135, A151, SCMFSA_2:60;
A153: h = <*i2,d2*> by A150, A152, Th24;
A154: dom <*i1,d2*> = {1,2} by FINSEQ_1:4, FINSEQ_3:29;
for k being set st k in {1,2} holds
<*i1,d2*> . k = f . k

proof

let k be set ; :: thesis:
assume A155: k in {1,2} ; :: thesis:

per cases by A155, TARSKI:def 2;

suppose A156: k = 1 ; :: thesis:

<*i1,d2*> . 1 = i1 by FINSEQ_1:61
.= f . 1 by A142, A149, FINSEQ_1:61 ;
hence <*i1,d2*> . k = f . k by A156; :: thesis:

end;

suppose A157: k = 2 ; :: thesis:

<*i1,d2*> . 2 = d2 by FINSEQ_1:61
.= f . 2 by A145, A153, FINSEQ_1:61 ;
hence <*i1,d2*> . k = f . k by A157; :: thesis:

end;

then A158: <*i1,d2*> = f by A137, A139, A154, FUNCT_1:9;
( InsCode (d2 =0_goto i1) = 7 & AddressPart (d2 =0_goto i1) = <*i1,d2*> ) by Th24, SCMFSA_2:48;
hence x in AddressParts T by A135, A136, A158; :: thesis:

end;

suppose A159: T = 8 ; :: thesis:

take product" (AddressParts T) ; :: according to CARD_3:def 14 :: thesis:
thus AddressParts T c= product (product" (AddressParts T)) by CARD_3:94; :: according to XBOOLE_0:def 10 :: thesis:
let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in product (product" (AddressParts T)) ; :: thesis:
then consider f being Function such that
A160: x = f and
A161: dom f = dom (product" (AddressParts T)) and
A162: for k being set st k in dom (product" (AddressParts T)) holds
f . k in (product" (AddressParts T)) . k by CARD_3:def 5;
A163: dom (product" (AddressParts T)) = {1,2} by A159, Th38;
then A164: 1 in dom (product" (AddressParts T)) by TARSKI:def 2;
then f . 1 in (product" (AddressParts T)) . 1 by A162;
then f . 1 in pi (AddressParts T),1 by A164, CARD_3:def 13;
then consider g being Function such that
A165: g in AddressParts T and
A166: g . 1 = f . 1 by CARD_3:def 6;
A167: 2 in dom (product" (AddressParts T)) by A163, TARSKI:def 2;
then f . 2 in (product" (AddressParts T)) . 2 by A162;
then f . 2 in pi (AddressParts T),2 by A167, CARD_3:def 13;
then consider h being Function such that
A168: h in AddressParts T and
A169: h . 2 = f . 2 by CARD_3:def 6;
consider I being Instruction of SCM+FSA such that
A170: g = AddressPart I and
A171: InsCode I = T by A165;
consider i1 being Instruction-Location of SCM+FSA , d1 being Int-Location such that
A172: I = d1 >0_goto i1 by A159, A171, SCMFSA_2:61;
A173: g = <*i1,d1*> by A170, A172, Th25;
consider J being Instruction of SCM+FSA such that
A174: h = AddressPart J and
A175: InsCode J = T by A168;
consider i2 being Instruction-Location of SCM+FSA , d2 being Int-Location such that
A176: J = d2 >0_goto i2 by A159, A175, SCMFSA_2:61;
A177: h = <*i2,d2*> by A174, A176, Th25;
A178: dom <*i1,d2*> = {1,2} by FINSEQ_1:4, FINSEQ_3:29;
for k being set st k in {1,2} holds
<*i1,d2*> . k = f . k

proof

let k be set ; :: thesis:
assume A179: k in {1,2} ; :: thesis:

per cases by A179, TARSKI:def 2;

suppose A180: k = 1 ; :: thesis:

<*i1,d2*> . 1 = i1 by FINSEQ_1:61
.= f . 1 by A166, A173, FINSEQ_1:61 ;
hence <*i1,d2*> . k = f . k by A180; :: thesis:

end;

suppose A181: k = 2 ; :: thesis:

<*i1,d2*> . 2 = d2 by FINSEQ_1:61
.= f . 2 by A169, A177, FINSEQ_1:61 ;
hence <*i1,d2*> . k = f . k by A181; :: thesis:

end;

then A182: <*i1,d2*> = f by A161, A163, A178, FUNCT_1:9;
( InsCode (d2 >0_goto i1) = 8 & AddressPart (d2 >0_goto i1) = <*i1,d2*> ) by Th25, SCMFSA_2:49;
hence x in AddressParts T by A159, A160, A182; :: thesis:

end;

suppose A183: T = 9 ; :: thesis:

take product" (AddressParts T) ; :: according to CARD_3:def 14 :: thesis:
thus AddressParts T c= product (product" (AddressParts T)) by CARD_3:94; :: according to XBOOLE_0:def 10 :: thesis:
let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in product (product" (AddressParts T)) ; :: thesis:
then consider f being Function such that
A184: x = f and
A185: dom f = dom (product" (AddressParts T)) and
A186: for k being set st k in dom (product" (AddressParts T)) holds
f . k in (product" (AddressParts T)) . k by CARD_3:def 5;
A187: dom (product" (AddressParts T)) = {1,2,3} by A183, Th39;
then A188: 1 in dom (product" (AddressParts T)) by ENUMSET1:def 1;
then f . 1 in (product" (AddressParts T)) . 1 by A186;
then f . 1 in pi (AddressParts T),1 by A188, CARD_3:def 13;
then consider g being Function such that
A189: g in AddressParts T and
A190: g . 1 = f . 1 by CARD_3:def 6;
A191: 2 in dom (product" (AddressParts T)) by A187, ENUMSET1:def 1;
then f . 2 in (product" (AddressParts T)) . 2 by A186;
then f . 2 in pi (AddressParts T),2 by A191, CARD_3:def 13;
then consider h being Function such that
A192: h in AddressParts T and
A193: h . 2 = f . 2 by CARD_3:def 6;
A194: 3 in dom (product" (AddressParts T)) by A187, ENUMSET1:def 1;
then f . 3 in (product" (AddressParts T)) . 3 by A186;
then f . 3 in pi (AddressParts T),3 by A194, CARD_3:def 13;
then consider z being Function such that
A195: z in AddressParts T and
A196: z . 3 = f . 3 by CARD_3:def 6;
consider I being Instruction of SCM+FSA such that
A197: g = AddressPart I and
A198: InsCode I = T by A189;
consider a, b being Int-Location , f1 being FinSeq-Location such that
A199: I = b := f1,a by A183, A198, SCMFSA_2:62;
A200: g = <*b,f1,a*> by A197, A199, MCART_1:def 2;
consider J being Instruction of SCM+FSA such that
A201: h = AddressPart J and
A202: InsCode J = T by A192;
consider d1, d2 being Int-Location , f2 being FinSeq-Location such that
A203: J = d2 := f2,d1 by A183, A202, SCMFSA_2:62;
A204: h = <*d2,f2,d1*> by A201, A203, MCART_1:def 2;
consider K being Instruction of SCM+FSA such that
A205: z = AddressPart K and
A206: InsCode K = T by A195;
consider d3, d4 being Int-Location , f3 being FinSeq-Location such that
A207: K = d4 := f3,d3 by A183, A206, SCMFSA_2:62;
A208: z = <*d4,f3,d3*> by A205, A207, MCART_1:def 2;
A209: dom <*b,f2,d3*> = {1,2,3} by FINSEQ_3:1, FINSEQ_3:30;
for k being set st k in {1,2,3} holds
<*b,f2,d3*> . k = f . k

proof

let k be set ; :: thesis:
assume A210: k in {1,2,3} ; :: thesis:

per cases by A210, ENUMSET1:def 1;

suppose A211: k = 1 ; :: thesis:

<*b,f2,d3*> . 1 = b by FINSEQ_1:62
.= f . 1 by A190, A200, FINSEQ_1:62 ;
hence <*b,f2,d3*> . k = f . k by A211; :: thesis:

end;

suppose A212: k = 2 ; :: thesis:

<*b,f2,d3*> . 2 = f2 by FINSEQ_1:62
.= f . 2 by A193, A204, FINSEQ_1:62 ;
hence <*b,f2,d3*> . k = f . k by A212; :: thesis:

end;

suppose A213: k = 3 ; :: thesis:

<*b,f2,d3*> . 3 = d3 by FINSEQ_1:62
.= f . 3 by A196, A208, FINSEQ_1:62 ;
hence <*b,f2,d3*> . k = f . k by A213; :: thesis:

end;

then A214: <*b,f2,d3*> = f by A185, A187, A209, FUNCT_1:9;
( InsCode (b := f2,d3) = 9 & AddressPart (b := f2,d3) = <*b,f2,d3*> ) by MCART_1:def 2, SCMFSA_2:50;
hence x in AddressParts T by A183, A184, A214; :: thesis:

end;

suppose A215: T = 10 ; :: thesis:

take product" (AddressParts T) ; :: according to CARD_3:def 14 :: thesis:
thus AddressParts T c= product (product" (AddressParts T)) by CARD_3:94; :: according to XBOOLE_0:def 10 :: thesis:
let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in product (product" (AddressParts T)) ; :: thesis:
then consider f being Function such that
A216: x = f and
A217: dom f = dom (product" (AddressParts T)) and
A218: for k being set st k in dom (product" (AddressParts T)) holds
f . k in (product" (AddressParts T)) . k by CARD_3:def 5;
A219: dom (product" (AddressParts T)) = {1,2,3} by A215, Th40;
then A220: 1 in dom (product" (AddressParts T)) by ENUMSET1:def 1;
then f . 1 in (product" (AddressParts T)) . 1 by A218;
then f . 1 in pi (AddressParts T),1 by A220, CARD_3:def 13;
then consider g being Function such that
A221: g in AddressParts T and
A222: g . 1 = f . 1 by CARD_3:def 6;
A223: 2 in dom (product" (AddressParts T)) by A219, ENUMSET1:def 1;
then f . 2 in (product" (AddressParts T)) . 2 by A218;
then f . 2 in pi (AddressParts T),2 by A223, CARD_3:def 13;
then consider h being Function such that
A224: h in AddressParts T and
A225: h . 2 = f . 2 by CARD_3:def 6;
A226: 3 in dom (product" (AddressParts T)) by A219, ENUMSET1:def 1;
then f . 3 in (product" (AddressParts T)) . 3 by A218;
then f . 3 in pi (AddressParts T),3 by A226, CARD_3:def 13;
then consider z being Function such that
A227: z in AddressParts T and
A228: z . 3 = f . 3 by CARD_3:def 6;
consider I being Instruction of SCM+FSA such that
A229: g = AddressPart I and
A230: InsCode I = T by A221;
consider a, b being Int-Location , f1 being FinSeq-Location such that
A231: I = f1,a := b by A215, A230, SCMFSA_2:63;
A232: g = <*b,f1,a*> by A229, A231, MCART_1:def 2;
consider J being Instruction of SCM+FSA such that
A233: h = AddressPart J and
A234: InsCode J = T by A224;
consider d1, d2 being Int-Location , f2 being FinSeq-Location such that
A235: J = f2,d1 := d2 by A215, A234, SCMFSA_2:63;
A236: h = <*d2,f2,d1*> by A233, A235, MCART_1:def 2;
consider K being Instruction of SCM+FSA such that
A237: z = AddressPart K and
A238: InsCode K = T by A227;
consider d3, d4 being Int-Location , f3 being FinSeq-Location such that
A239: K = f3,d3 := d4 by A215, A238, SCMFSA_2:63;
A240: z = <*d4,f3,d3*> by A237, A239, MCART_1:def 2;
A241: dom <*b,f2,d3*> = {1,2,3} by FINSEQ_3:1, FINSEQ_3:30;
for k being set st k in {1,2,3} holds
<*b,f2,d3*> . k = f . k

proof

let k be set ; :: thesis:
assume A242: k in {1,2,3} ; :: thesis:

per cases by A242, ENUMSET1:def 1;

suppose A243: k = 1 ; :: thesis:

<*b,f2,d3*> . 1 = b by FINSEQ_1:62
.= f . 1 by A222, A232, FINSEQ_1:62 ;
hence <*b,f2,d3*> . k = f . k by A243; :: thesis:

end;

suppose A244: k = 2 ; :: thesis:

<*b,f2,d3*> . 2 = f2 by FINSEQ_1:62
.= f . 2 by A225, A236, FINSEQ_1:62 ;
hence <*b,f2,d3*> . k = f . k by A244; :: thesis:

end;

suppose A245: k = 3 ; :: thesis:

<*b,f2,d3*> . 3 = d3 by FINSEQ_1:62
.= f . 3 by A228, A240, FINSEQ_1:62 ;
hence <*b,f2,d3*> . k = f . k by A245; :: thesis:

end;

then A246: <*b,f2,d3*> = f by A217, A219, A241, FUNCT_1:9;
( InsCode (f2,d3 := b) = 10 & AddressPart (f2,d3 := b) = <*b,f2,d3*> ) by MCART_1:def 2, SCMFSA_2:51;
hence x in AddressParts T by A215, A216, A246; :: thesis:

end;

suppose A247: T = 11 ; :: thesis:

take product" (AddressParts T) ; :: according to CARD_3:def 14 :: thesis:
thus AddressParts T c= product (product" (AddressParts T)) by CARD_3:94; :: according to XBOOLE_0:def 10 :: thesis:
let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in product (product" (AddressParts T)) ; :: thesis:
then consider f being Function such that
A248: x = f and
A249: dom f = dom (product" (AddressParts T)) and
A250: for k being set st k in dom (product" (AddressParts T)) holds
f . k in (product" (AddressParts T)) . k by CARD_3:def 5;
A251: dom (product" (AddressParts T)) = {1,2} by A247, Th41;
then A252: 1 in dom (product" (AddressParts T)) by TARSKI:def 2;
then f . 1 in (product" (AddressParts T)) . 1 by A250;
then f . 1 in pi (AddressParts T),1 by A252, CARD_3:def 13;
then consider g being Function such that
A253: g in AddressParts T and
A254: g . 1 = f . 1 by CARD_3:def 6;
A255: 2 in dom (product" (AddressParts T)) by A251, TARSKI:def 2;
then f . 2 in (product" (AddressParts T)) . 2 by A250;
then f . 2 in pi (AddressParts T),2 by A255, CARD_3:def 13;
then consider h being Function such that
A256: h in AddressParts T and
A257: h . 2 = f . 2 by CARD_3:def 6;
consider I being Instruction of SCM+FSA such that
A258: g = AddressPart I and
A259: InsCode I = T by A253;
consider a being Int-Location , f1 being FinSeq-Location such that
A260: I = a :=len f1 by A247, A259, SCMFSA_2:64;
A261: g = <*a,f1*> by A258, A260, MCART_1:def 2;
consider J being Instruction of SCM+FSA such that
A262: h = AddressPart J and
A263: InsCode J = T by A256;
consider b being Int-Location , f2 being FinSeq-Location such that
A264: J = b :=len f2 by A247, A263, SCMFSA_2:64;
A265: h = <*b,f2*> by A262, A264, MCART_1:def 2;
A266: dom <*a,f2*> = {1,2} by FINSEQ_1:4, FINSEQ_3:29;
for k being set st k in {1,2} holds
<*a,f2*> . k = f . k

proof

let k be set ; :: thesis:
assume A267: k in {1,2} ; :: thesis:

per cases by A267, TARSKI:def 2;

suppose A268: k = 1 ; :: thesis:

<*a,f2*> . 1 = a by FINSEQ_1:61
.= f . 1 by A254, A261, FINSEQ_1:61 ;
hence <*a,f2*> . k = f . k by A268; :: thesis:

end;

suppose A269: k = 2 ; :: thesis:

<*a,f2*> . 2 = f2 by FINSEQ_1:61
.= f . 2 by A257, A265, FINSEQ_1:61 ;
hence <*a,f2*> . k = f . k by A269; :: thesis:

end;

then A270: <*a,f2*> = f by A249, A251, A266, FUNCT_1:9;
( InsCode (a :=len f2) = 11 & AddressPart (a :=len f2) = <*a,f2*> ) by MCART_1:def 2, SCMFSA_2:52;
hence x in AddressParts T by A247, A248, A270; :: thesis:

end;

suppose A271: T = 12 ; :: thesis:

take product" (AddressParts T) ; :: according to CARD_3:def 14 :: thesis:
thus AddressParts T c= product (product" (AddressParts T)) by CARD_3:94; :: according to XBOOLE_0:def 10 :: thesis:
let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in product (product" (AddressParts T)) ; :: thesis:
then consider f being Function such that
A272: x = f and
A273: dom f = dom (product" (AddressParts T)) and
A274: for k being set st k in dom (product" (AddressParts T)) holds
f . k in (product" (AddressParts T)) . k by CARD_3:def 5;
A275: dom (product" (AddressParts T)) = {1,2} by A271, Th42;
then A276: 1 in dom (product" (AddressParts T)) by TARSKI:def 2;
then f . 1 in (product" (AddressParts T)) . 1 by A274;
then f . 1 in pi (AddressParts T),1 by A276, CARD_3:def 13;
then consider g being Function such that
A277: g in AddressParts T and
A278: g . 1 = f . 1 by CARD_3:def 6;
A279: 2 in dom (product" (AddressParts T)) by A275, TARSKI:def 2;
then f . 2 in (product" (AddressParts T)) . 2 by A274;
then f . 2 in pi (AddressParts T),2 by A279, CARD_3:def 13;
then consider h being Function such that
A280: h in AddressParts T and
A281: h . 2 = f . 2 by CARD_3:def 6;
consider I being Instruction of SCM+FSA such that
A282: g = AddressPart I and
A283: InsCode I = T by A277;
consider a being Int-Location , f1 being FinSeq-Location such that
A284: I = f1 :=<0,...,0> a by A271, A283, SCMFSA_2:65;
A285: g = <*a,f1*> by A282, A284, MCART_1:def 2;
consider J being Instruction of SCM+FSA such that
A286: h = AddressPart J and
A287: InsCode J = T by A280;
consider b being Int-Location , f2 being FinSeq-Location such that
A288: J = f2 :=<0,...,0> b by A271, A287, SCMFSA_2:65;
A289: h = <*b,f2*> by A286, A288, MCART_1:def 2;
A290: dom <*a,f2*> = {1,2} by FINSEQ_1:4, FINSEQ_3:29;
for k being set st k in {1,2} holds
<*a,f2*> . k = f . k

proof

let k be set ; :: thesis:
assume A291: k in {1,2} ; :: thesis:

per cases by A291, TARSKI:def 2;

suppose A292: k = 1 ; :: thesis:

<*a,f2*> . 1 = a by FINSEQ_1:61
.= f . 1 by A278, A285, FINSEQ_1:61 ;
hence <*a,f2*> . k = f . k by A292; :: thesis:

end;

suppose A293: k = 2 ; :: thesis:

<*a,f2*> . 2 = f2 by FINSEQ_1:61
.= f . 2 by A281, A289, FINSEQ_1:61 ;
hence <*a,f2*> . k = f . k by A293; :: thesis:

end;

then A294: <*a,f2*> = f by A273, A275, A290, FUNCT_1:9;
( InsCode (f2 :=<0,...,0> a) = 12 & AddressPart (f2 :=<0,...,0> a) = <*a,f2*> ) by MCART_1:def 2, SCMFSA_2:53;
hence x in AddressParts T by A271, A272, A294; :: thesis:

end;