let N be with_non-empty_elements set ; :: thesis: for IL being non trivial set
for S being non empty stored-program standard-ins homogeneous AMI-Struct of IL,N
for I being Instruction of S
for x being set st x in dom (AddressPart I) & (product" (AddressParts (InsCode I))) . x = IL holds
(AddressPart I) . x is Instruction-Location of S
let IL be non trivial set ; :: thesis: for S being non empty stored-program standard-ins homogeneous AMI-Struct of IL,N
for I being Instruction of S
for x being set st x in dom (AddressPart I) & (product" (AddressParts (InsCode I))) . x = IL holds
(AddressPart I) . x is Instruction-Location of S
let S be non empty stored-program standard-ins homogeneous AMI-Struct of IL,N; :: thesis: for I being Instruction of S
for x being set st x in dom (AddressPart I) & (product" (AddressParts (InsCode I))) . x = IL holds
(AddressPart I) . x is Instruction-Location of S
let I be Instruction of S; :: thesis: for x being set st x in dom (AddressPart I) & (product" (AddressParts (InsCode I))) . x = IL holds
(AddressPart I) . x is Instruction-Location of S
let x be set ; :: thesis: ( x in dom (AddressPart I) & (product" (AddressParts (InsCode I))) . x = IL implies (AddressPart I) . x is Instruction-Location of S )
assume A1: x in dom (AddressPart I) ; :: thesis: ( not (product" (AddressParts (InsCode I))) . x = IL or (AddressPart I) . x is Instruction-Location of S )
A2: AddressPart I in AddressParts (InsCode I) ;
assume A3: (product" (AddressParts (InsCode I))) . x = IL ; :: 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 S 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 IL by A2, A3, CARD_3:def 6;
hence (AddressPart I) . x is Instruction-Location of S by AMI_1:def 4; :: thesis: verum