let S be standard-ins homogeneous regular COM-Struct ; :: thesis: for I being Instruction of S
for x being set st x in dom (JumpPart I) holds
(JumpPart I) . x is Element of NAT
let I be Instruction of S; :: thesis: for x being set st x in dom (JumpPart I) holds
(JumpPart I) . x is Element of NAT
let x be set ; :: thesis: ( x in dom (JumpPart I) implies (JumpPart I) . x is Element of NAT )
assume A1: x in dom (JumpPart I) ; :: thesis: (JumpPart I) . x is Element of NAT
A2: JumpPart I in JumpParts (InsCode I) ;
A3: (product" (JumpParts (InsCode I))) . x = NAT by A1, Def35;
for f being Function st f in JumpParts (InsCode I) holds
x in dom f

proof

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

end;

then x in dom (product" (JumpParts (InsCode I))) by CARD_3:def 12;
then (product" (JumpParts (InsCode I))) . x = pi ((JumpParts (InsCode I)),x) by CARD_3:def 12;
hence (JumpPart I) . x is Element of NAT by A2, A3, CARD_3:def 6; :: thesis: verum