set D = (union N) \/ the carrier of S;
defpred S₁[ set , set ] means ( ( (product" (AddressParts (InsCode I))) . $1 = NAT implies ex il being Instruction-Location of S st
( il = (AddressPart I) . $1 & $2 = il. S,(k + (locnum il)) ) ) & ( (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 (union N) \/ the carrier of S st S₁[m,x]

proof

let m be Nat; :: thesis: ( m in Seg (len (AddressPart I)) implies ex x being Element of (union N) \/ the carrier of S st S₁[m,x] )
assume m in Seg (len (AddressPart I)) ; :: thesis: ex x being Element of (union N) \/ the carrier of S st S₁[m,x]
then A2: m in dom (AddressPart I) by FINSEQ_1:def 3;
then A3: (AddressPart I) . m in rng (AddressPart I) by FUNCT_1:def 5;

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 (union N) \/ the carrier of S st S₁[m,x]

then reconsider il = (AddressPart I) . m as Instruction-Location of S by A2, Th20;
reconsider x = il. S,(k + (locnum il)) as Element of (union N) \/ the carrier of S 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 (union N) \/ the carrier of S st S₁[m,x]

reconsider x = (AddressPart I) . m as Element of (union N) \/ the carrier of S by A3;
take x ; :: thesis: S₁[m,x]
thus S₁[m,x] by A5; :: thesis: verum

end;

end;

end;

consider p being FinSequence of (union N) \/ the carrier of S 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 Instruction-Location of S st
( il = (AddressPart I) . z & p . z = il. S,(k + (locnum il)) ) by A6, A7, A11;
hence p . z in (product" (AddressParts (InsCode I))) . z by A13, AMI_1:def 4; :: 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 Instruction-Location of S st
( f = (AddressPart I) . n & (AddressPart IT) . n = il. S,(k + (locnum f)) ) ) & ( (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 Instruction-Location of S st
( f = (AddressPart I) . n & (AddressPart IT) . n = il. S,(k + (locnum f)) ) ) & ( (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 Instruction-Location of S st
( f = (AddressPart I) . n & (AddressPart IT) . n = il. S,(k + (locnum f)) ) ) & ( (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 Instruction-Location of S st
( f = (AddressPart I) . n & (AddressPart IT) . n = il. S,(k + (locnum f)) ) ) & ( (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 Instruction-Location of S st
( f = (AddressPart I) . n & (AddressPart IT) . n = il. S,(k + (locnum f)) ) ) & ( (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 Instruction-Location of S st
( f = (AddressPart I) . n & (AddressPart IT) . n = il. S,(k + (locnum f)) ) ) & ( (product" (AddressParts (InsCode I))) . n <> NAT implies (AddressPart IT) . n = (AddressPart I) . n ) ) by A7, A14; :: thesis: verum