let N be with_non-empty_elements set ; :: thesis: for S being non empty stored-program standard-ins homogeneous AMI-Struct of N
for I being Instruction of
for x being set st x in dom (AddressPart I) & (product" (AddressParts (InsCode I))) . x = NAT holds
(AddressPart I) . x is Instruction-Location of S
let S be non empty stored-program standard-ins homogeneous AMI-Struct of N; :: thesis: for I being Instruction of
for x being set st x in dom (AddressPart I) & (product" (AddressParts (InsCode I))) . x = NAT holds
(AddressPart I) . x is Instruction-Location of S
let I be Instruction of ; :: thesis: for x being set st x in dom (AddressPart I) & (product" (AddressParts (InsCode I))) . x = NAT holds
(AddressPart I) . x is Instruction-Location of S
let x be set ; :: thesis: ( x in dom (AddressPart I) & (product" (AddressParts (InsCode I))) . x = NAT implies (AddressPart I) . x is Instruction-Location of S )
assume A1: x in dom (AddressPart I) ; :: thesis: ( not (product" (AddressParts (InsCode I))) . x = NAT or (AddressPart I) . x is Instruction-Location of S )
A2: AddressPart I in AddressParts (InsCode I) ;
assume A3: (product" (AddressParts (InsCode I))) . x = NAT ; :: thesis: (AddressPart I) . x is Instruction-Location of S
for f being Function st f in AddressParts (InsCode I) holds
x in dom f

proof

let f be Function; :: thesis: ( f in AddressParts (InsCode I) implies x in dom f )
assume f in AddressParts (InsCode I) ; :: thesis: x in dom f
then ex J being Instruction of st
( f = AddressPart J & InsCode I = InsCode J ) ;
hence x in dom f by A1, Def4; :: thesis: verum

end;

then x in dom (product" (AddressParts (InsCode I))) by A2, CARD_3:def 13;
then (product" (AddressParts (InsCode I))) . x = pi (AddressParts (InsCode I)),x by A2, CARD_3:def 13;
then (AddressPart I) . x is Element of NAT by A2, A3, CARD_3:def 6;
hence (AddressPart I) . x is Instruction-Location of S by AMI_1:def 4; :: thesis: verum