let a, b be Instruction of S; :: thesis: ( InsCode a = InsCode I & dom (AddressPart a) = 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 a) . n = il. S,(k + (locnum f)) ) ) & ( (product" (AddressParts (InsCode I))) . n <> NAT implies (AddressPart a) . n = (AddressPart I) . n ) ) ) & InsCode b = InsCode I & dom (AddressPart b) = 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 b) . n = il. S,(k + (locnum f)) ) ) & ( (product" (AddressParts (InsCode I))) . n <> NAT implies (AddressPart b) . n = (AddressPart I) . n ) ) ) implies a = b )
assume that
A17: InsCode a = InsCode I and
A18: dom (AddressPart a) = dom (AddressPart I) and
A19: 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 a) . n = il. S,(k + (locnum f)) ) ) & ( (product" (AddressParts (InsCode I))) . n <> NAT implies (AddressPart a) . n = (AddressPart I) . n ) ) and
A20: InsCode b = InsCode I and
A21: dom (AddressPart b) = dom (AddressPart I) and
A22: 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 b) . n = il. S,(k + (locnum f)) ) ) & ( (product" (AddressParts (InsCode I))) . n <> NAT implies (AddressPart b) . n = (AddressPart I) . n ) ) ; :: thesis: a = b
A23: Seg (len (AddressPart a)) = dom (AddressPart a) by FINSEQ_1:def 3;
for n being Nat st n in Seg (len (AddressPart a)) holds
(AddressPart a) . n = (AddressPart b) . n

proof

let n be Nat; :: thesis: ( n in Seg (len (AddressPart a)) implies (AddressPart a) . n = (AddressPart b) . n )
assume n in Seg (len (AddressPart a)) ; :: thesis: (AddressPart a) . n = (AddressPart b) . n
then ( ( (product" (AddressParts (InsCode I))) . n = NAT implies ex f being Instruction-Location of S st
( f = (AddressPart I) . n & (AddressPart a) . n = il. S,(k + (locnum f)) ) ) & ( (product" (AddressParts (InsCode I))) . n <> NAT implies (AddressPart a) . n = (AddressPart I) . n ) & ( (product" (AddressParts (InsCode I))) . n = NAT implies ex f being Instruction-Location of S st
( f = (AddressPart I) . n & (AddressPart b) . n = il. S,(k + (locnum f)) ) ) & ( (product" (AddressParts (InsCode I))) . n <> NAT implies (AddressPart b) . n = (AddressPart I) . n ) ) by A18, A19, A22, A23;
hence (AddressPart a) . n = (AddressPart b) . n ; :: thesis: verum

end;

hence a = b by A17, A20, Th16, A18, A21, A23, FINSEQ_1:17; :: thesis: verum