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