consider D0 being non empty set such that
W: the Instructions of S c= [:NAT ,(D0 * ):] by AMI_1:def 32;
set D = D0 \/ NAT ;
defpred S₁[ set , set ] means ( ( (product" (AddressParts (InsCode I))) . $1 = NAT implies ex il being Element of NAT st
( il = (AddressPart I) . $1 & $2 = il. S,(k + (locnum il,S)) ) ) & ( (product" (AddressParts (InsCode I))) . $1 <> NAT implies $2 = (AddressPart I) . $1 ) );
A1: for m being Nat st m in Seg (len (AddressPart I)) holds
ex x being Element of D0 \/ NAT st S₁[m,x]

proof

let m be Nat; :: thesis: ( m in Seg (len (AddressPart I)) implies ex x being Element of D0 \/ NAT st S₁[m,x] )
assume m in Seg (len (AddressPart I)) ; :: thesis: ex x being Element of D0 \/ NAT st S₁[m,x]
then A2: m in dom (AddressPart I) by FINSEQ_1:def 3;
D0 c= D0 \/ NAT by XBOOLE_1:7;
then D0 * c= (D0 \/ NAT ) * by FINSEQ_1:83;
then C: [:NAT ,(D0 * ):] c= [:NAT ,((D0 \/ NAT ) * ):] by ZFMISC_1:118;
I in the Instructions of S ;
then I in [:NAT ,(D0 * ):] by W;
then B1: I in [:NAT ,((D0 \/ NAT ) * ):] by C;

per cases ( (product" (AddressParts (InsCode I))) . m = NAT or (product" (AddressParts (InsCode I))) . m <> NAT ) ;

suppose A4: (product" (AddressParts (InsCode I))) . m = NAT ; :: thesis: ex x being Element of D0 \/ NAT st S₁[m,x]

then reconsider il = (AddressPart I) . m as Element of NAT by A2, Th20;
reconsider x = il. S,(k + (locnum il,S)) as Element of D0 \/ NAT by XBOOLE_0:def 3;
take x ; :: thesis: S₁[m,x]
thus S₁[m,x] by A4; :: thesis: verum

end;

suppose A5: (product" (AddressParts (InsCode I))) . m <> NAT ; :: thesis: ex x being Element of D0 \/ NAT st S₁[m,x]

AddressPart I in (D0 \/ NAT ) * by B1, MCART_1:10;
then (AddressPart I) . m in D0 \/ NAT by A2, FINSEQ_1:105;
then reconsider x = (AddressPart I) . m as Element of D0 \/ NAT ;
take x ; :: thesis: S₁[m,x]
thus S₁[m,x] by A5; :: thesis: verum

end;

end;

end;

consider p being FinSequence of D0 \/ NAT such that
A6: dom p = Seg (len (AddressPart I)) and
A7: for k being Nat st k in Seg (len (AddressPart I)) holds
S₁[k,p . k] from FINSEQ_1:sch 5(A1);
set f = product" (AddressParts (InsCode I));
A8: AddressPart I in AddressParts (InsCode I) ;
then A9: AddressParts (InsCode I) = product (product" (AddressParts (InsCode I))) by CARD_3:95;
A10: dom p = dom (AddressPart I) by A6, FINSEQ_1:def 3
.= DOM (AddressParts (InsCode I)) by A8, CARD_3:def 12
.= dom (product" (AddressParts (InsCode I))) by CARD_3:92 ;
for z being set st z in dom p holds
p . z in (product" (AddressParts (InsCode I))) . z

proof

let z be set ; :: thesis: ( z in dom p implies p . z in (product" (AddressParts (InsCode I))) . z )
assume A11: z in dom p ; :: thesis: p . z in (product" (AddressParts (InsCode I))) . z
then A12: (product" (AddressParts (InsCode I))) . z = pi (AddressParts (InsCode I)),z by A8, A10, CARD_3:def 13;
reconsider z = z as Element of NAT by A11;

per cases ( (product" (AddressParts (InsCode I))) . z = NAT or (product" (AddressParts (InsCode I))) . z <> NAT ) ;

suppose A13: (product" (AddressParts (InsCode I))) . z = NAT ; :: thesis: p . z in (product" (AddressParts (InsCode I))) . z

then ex il being Element of NAT st
( il = (AddressPart I) . z & p . z = il. S,(k + (locnum il,S)) ) by A6, A7, A11;
hence p . z in (product" (AddressParts (InsCode I))) . z by A13; :: thesis: verum

end;

suppose (product" (AddressParts (InsCode I))) . z <> NAT ; :: thesis: p . z in (product" (AddressParts (InsCode I))) . z

then p . z = (AddressPart I) . z by A6, A7, A11;
hence p . z in (product" (AddressParts (InsCode I))) . z by A8, A12, CARD_3:def 6; :: thesis: verum

end;

end;

end;

then p in AddressParts (InsCode I) by A9, A10, CARD_3:18;
then consider IT being Instruction of S such that
A14: p = AddressPart IT and
A15: InsCode I = InsCode IT ;
take IT ; :: thesis: ( InsCode IT = InsCode I & dom (AddressPart IT) = dom (AddressPart I) & ( for n being set st n in dom (AddressPart I) holds
( ( (product" (AddressParts (InsCode I))) . n = NAT implies ex f being Element of NAT st
( f = (AddressPart I) . n & (AddressPart IT) . n = il. S,(k + (locnum f,S)) ) ) & ( (product" (AddressParts (InsCode I))) . n <> NAT implies (AddressPart IT) . n = (AddressPart I) . n ) ) ) )
thus InsCode IT = InsCode I by A15; :: thesis: ( dom (AddressPart IT) = dom (AddressPart I) & ( for n being set st n in dom (AddressPart I) holds
( ( (product" (AddressParts (InsCode I))) . n = NAT implies ex f being Element of NAT st
( f = (AddressPart I) . n & (AddressPart IT) . n = il. S,(k + (locnum f,S)) ) ) & ( (product" (AddressParts (InsCode I))) . n <> NAT implies (AddressPart IT) . n = (AddressPart I) . n ) ) ) )
thus dom (AddressPart IT) = dom (AddressPart I) by A6, A14, FINSEQ_1:def 3; :: thesis: for n being set st n in dom (AddressPart I) holds
( ( (product" (AddressParts (InsCode I))) . n = NAT implies ex f being Element of NAT st
( f = (AddressPart I) . n & (AddressPart IT) . n = il. S,(k + (locnum f,S)) ) ) & ( (product" (AddressParts (InsCode I))) . n <> NAT implies (AddressPart IT) . n = (AddressPart I) . n ) )
let n be set ; :: thesis: ( n in dom (AddressPart I) implies ( ( (product" (AddressParts (InsCode I))) . n = NAT implies ex f being Element of NAT st
( f = (AddressPart I) . n & (AddressPart IT) . n = il. S,(k + (locnum f,S)) ) ) & ( (product" (AddressParts (InsCode I))) . n <> NAT implies (AddressPart IT) . n = (AddressPart I) . n ) ) )
assume A16: n in dom (AddressPart I) ; :: thesis: ( ( (product" (AddressParts (InsCode I))) . n = NAT implies ex f being Element of NAT st
( f = (AddressPart I) . n & (AddressPart IT) . n = il. S,(k + (locnum f,S)) ) ) & ( (product" (AddressParts (InsCode I))) . n <> NAT implies (AddressPart IT) . n = (AddressPart I) . n ) )
then reconsider n = n as Element of NAT ;
n in Seg (len (AddressPart I)) by A16, FINSEQ_1:def 3;
hence ( ( (product" (AddressParts (InsCode I))) . n = NAT implies ex f being Element of NAT st
( f = (AddressPart I) . n & (AddressPart IT) . n = il. S,(k + (locnum f,S)) ) ) & ( (product" (AddressParts (InsCode I))) . n <> NAT implies (AddressPart IT) . n = (AddressPart I) . n ) ) by A7, A14; :: thesis: verum