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 Element of NAT st
( f = (AddressPart I) . n & (AddressPart a) . n = il. S,(k + (locnum f,S)) ) ) & ( (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 Element of NAT st
( f = (AddressPart I) . n & (AddressPart b) . n = il. S,(k + (locnum f,S)) ) ) & ( (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 Element of NAT st
( f = (AddressPart I) . n & (AddressPart a) . n = il. S,(k + (locnum f,S)) ) ) & ( (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 Element of NAT st
( f = (AddressPart I) . n & (AddressPart b) . n = il. S,(k + (locnum f,S)) ) ) & ( (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 A24: n in Seg (len (AddressPart a)) ; :: thesis: (AddressPart a) . n = (AddressPart b) . n
then A25: ( (product" (AddressParts (InsCode I))) . n = NAT implies ex f being Element of NAT st
( f = (AddressPart I) . n & (AddressPart a) . n = il. S,(k + (locnum f,S)) ) ) by A18, A19, A23;
A26: ( (product" (AddressParts (InsCode I))) . n <> NAT implies (AddressPart a) . n = (AddressPart I) . n ) by A18, A19, A23, A24;
( (product" (AddressParts (InsCode I))) . n = NAT implies ex f being Element of NAT st
( f = (AddressPart I) . n & (AddressPart b) . n = il. S,(k + (locnum f,S)) ) ) by A18, A22, A23, A24;
hence (AddressPart a) . n = (AddressPart b) . n by A18, A22, A23, A24, A25, A26; :: thesis: verum

end;

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