consider y being set such that
B1: [T,y] in proj1 the Instructions of S by RELAT_1:def 4;
consider z being set such that
A1: [[T,y],z] in the Instructions of S by B1, RELAT_1:def 4;
reconsider I = [T,y,z] as Instruction of S by A1;
X1: InsCode I = T by RECDEF_2:def 1;
X4: JumpPart I = y by RECDEF_2:def 2;
set f = (dom (JumpPart I)) --> NAT ;
D1: dom ((dom (JumpPart I)) --> NAT ) = dom (JumpPart I) by FUNCOP_1:19;
for x being set holds
( x in JumpParts T iff ex g being Function st
( x = g & dom g = dom ((dom (JumpPart I)) --> NAT ) & ( for y being set st y in dom ((dom (JumpPart I)) --> NAT ) holds
g . y in ((dom (JumpPart I)) --> NAT ) . y ) ) )

proof

let x be set ; :: thesis: ( x in JumpParts T iff ex g being Function st
( x = g & dom g = dom ((dom (JumpPart I)) --> NAT ) & ( for y being set st y in dom ((dom (JumpPart I)) --> NAT ) holds
g . y in ((dom (JumpPart I)) --> NAT ) . y ) ) )
thus ( x in JumpParts T implies ex g being Function st
( x = g & dom g = dom ((dom (JumpPart I)) --> NAT ) & ( for y being set st y in dom ((dom (JumpPart I)) --> NAT ) holds
g . y in ((dom (JumpPart I)) --> NAT ) . y ) ) ) :: thesis: ( ex g being Function st
( x = g & dom g = dom ((dom (JumpPart I)) --> NAT ) & ( for y being set st y in dom ((dom (JumpPart I)) --> NAT ) holds
g . y in ((dom (JumpPart I)) --> NAT ) . y ) ) implies x in JumpParts T )

proof

assume x in JumpParts T ; :: thesis: ex g being Function st
( x = g & dom g = dom ((dom (JumpPart I)) --> NAT ) & ( for y being set st y in dom ((dom (JumpPart I)) --> NAT ) holds
g . y in ((dom (JumpPart I)) --> NAT ) . y ) )
then consider K being Instruction of S such that
W1: x = JumpPart K and
W2: InsCode K = T ;
take g = JumpPart K; :: thesis: ( x = g & dom g = dom ((dom (JumpPart I)) --> NAT ) & ( for y being set st y in dom ((dom (JumpPart I)) --> NAT ) holds
g . y in ((dom (JumpPart I)) --> NAT ) . y ) )
thus x = g by W1; :: thesis: ( dom g = dom ((dom (JumpPart I)) --> NAT ) & ( for y being set st y in dom ((dom (JumpPart I)) --> NAT ) holds
g . y in ((dom (JumpPart I)) --> NAT ) . y ) )
thus K: dom g = dom ((dom (JumpPart I)) --> NAT ) by W2, X1, Def4, D1; :: thesis: for y being set st y in dom ((dom (JumpPart I)) --> NAT ) holds
g . y in ((dom (JumpPart I)) --> NAT ) . y
let y be set ; :: thesis: ( y in dom ((dom (JumpPart I)) --> NAT ) implies g . y in ((dom (JumpPart I)) --> NAT ) . y )
assume Z: y in dom ((dom (JumpPart I)) --> NAT ) ; :: thesis: g . y in ((dom (JumpPart I)) --> NAT ) . y
then ((dom (JumpPart I)) --> NAT ) . y = NAT by D1, FUNCOP_1:13;
hence g . y in ((dom (JumpPart I)) --> NAT ) . y by K, Z, FUNCT_1:172; :: thesis: verum

end;

given g being Function such that G1: x = g and
G2: dom g = dom ((dom (JumpPart I)) --> NAT ) and
G3: for y being set st y in dom ((dom (JumpPart I)) --> NAT ) holds
g . y in ((dom (JumpPart I)) --> NAT ) . y ; :: thesis: x in JumpParts T
X3: dom g = dom (JumpPart I) by G2, FUNCOP_1:19;
set J = [T,g,z];
Y1: y in JumpParts T by X4, X1;
then X6: dom g = dom (product" (JumpParts T)) by X3, X4, CARD_3:150;
for x being set st x in dom (product" (JumpParts T)) holds
g . x in (product" (JumpParts T)) . x

proof

let x be set ; :: thesis: ( x in dom (product" (JumpParts T)) implies g . x in (product" (JumpParts T)) . x )
assume Z: x in dom (product" (JumpParts T)) ; :: thesis: g . x in (product" (JumpParts T)) . x
((dom (JumpPart I)) --> NAT ) . x = NAT by X6, X3, Z, FUNCOP_1:13;
then g . x in NAT by G3, X6, Z, G2;
hence g . x in (product" (JumpParts T)) . x by Z, X6, X1, X3, Def11; :: thesis: verum

end;

then X5: g in product (product" (JumpParts T)) by X6, CARD_3:18;
reconsider J = [T,g,z] as Instruction of S by Y1, Dfs, X4, X5;
X2: InsCode J = T by RECDEF_2:def 1;
g = JumpPart J by RECDEF_2:def 2;
hence x in JumpParts T by X2, G1; :: thesis: verum

end;

then JumpParts T = product ((dom (JumpPart I)) --> NAT ) by CARD_3:def 5;
hence JumpParts T is product-like ; :: thesis: verum