JumpPart I is NAT -valued

proof

let x be set ; :: according to RELAT_1:def 19,TARSKI:def 3 :: thesis: ( not x in proj2 (JumpPart I) or x in NAT )
assume x in rng (JumpPart I) ; :: thesis: x in NAT
then consider k being set such that
A1: k in dom (JumpPart I) and
A2: (JumpPart I) . k = x by FUNCT_1:def 3;
set X = JumpParts (InsCode I);
A3: JumpPart I in JumpParts (InsCode I) ;
then k in dom (product" (JumpParts (InsCode I))) by A1, CARD_3:100;
then (JumpPart I) . k in (product" (JumpParts (InsCode I))) . k by A3, CARD_3:101;
hence x in NAT by A1, A2, Def35; :: thesis: verum

end;

hence for b₁ being Function st b₁ = JumpPart I holds
b₁ is NAT -valued ; :: thesis: verum