let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program standard-ins regular AMI-Struct of N
for I being Instruction of S
for x being set st x in dom (AddressPart I) holds
(AddressPart I) . x in (product" (AddressParts (InsCode I))) . x
let S be non empty stored-program standard-ins regular AMI-Struct of N; :: thesis: for I being Instruction of S
for x being set st x in dom (AddressPart I) holds
(AddressPart I) . x in (product" (AddressParts (InsCode I))) . x
let I be Instruction of S; :: thesis: for x being set st x in dom (AddressPart I) holds
(AddressPart I) . x in (product" (AddressParts (InsCode I))) . x
let x be set ; :: thesis: ( x in dom (AddressPart I) implies (AddressPart I) . x in (product" (AddressParts (InsCode I))) . x )
assume A1: x in dom (AddressPart I) ; :: thesis: (AddressPart I) . x in (product" (AddressParts (InsCode I))) . x
A2: AddressPart I in AddressParts (InsCode I) ;
A3: dom (product" (AddressParts (InsCode I))) = DOM (AddressParts (InsCode I)) by CARD_3:92
.= dom (AddressPart I) by A2, CARD_3:def 12 ;
(AddressPart I) . x in pi (AddressParts (InsCode I)),x by A2, CARD_3:def 6;
hence (AddressPart I) . x in (product" (AddressParts (InsCode I))) . x by A1, A3, CARD_3:93; :: thesis: verum