consider y being set such that
A1: [T,y] in proj1 the Instructions of S by RELAT_1:def 4;
consider z being set such that
A2: [[T,y],z] in the Instructions of S by A1, RELAT_1:def 4;
reconsider I = [T,y,z] as Instruction of S by A2;
A3: InsCode I = T by RECDEF_2:def 1;
A4: JumpPart I = y by RECDEF_2:def 2;
set f = (dom (JumpPart I)) --> NAT;
A5: dom ((dom (JumpPart I)) --> NAT) = dom (JumpPart I) by FUNCOP_1:13;
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
A6: x = JumpPart K and
A7: 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 A6; :: 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 A8: dom g = dom ((dom (JumpPart I)) --> NAT) by A7, A3, Def33, A5; :: 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 A9: y in dom ((dom (JumpPart I)) --> NAT) ; :: thesis: g . y in ((dom (JumpPart I)) --> NAT) . y
then ((dom (JumpPart I)) --> NAT) . y = NAT by A5, FUNCOP_1:7;
hence g . y in ((dom (JumpPart I)) --> NAT) . y by A8, A9, FUNCT_1:102; :: thesis: verum

end;

given g being Function such that A10: x = g and
A11: dom g = dom ((dom (JumpPart I)) --> NAT) and
A12: 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
A13: dom g = dom (JumpPart I) by A11, FUNCOP_1:13;
set J = [T,g,z];
A14: y in JumpParts T by A4, A3;
then A15: dom g = dom (product" (JumpParts T)) by A13, A4, CARD_3:100;
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 A16: x in dom (product" (JumpParts T)) ; :: thesis: g . x in (product" (JumpParts T)) . x
((dom (JumpPart I)) --> NAT) . x = NAT by A15, A13, A16, FUNCOP_1:7;
then g . x in NAT by A12, A15, A16, A11;
hence g . x in (product" (JumpParts T)) . x by A16, A15, A3, A13, Def35; :: thesis: verum

end;

then A17: g in product (product" (JumpParts T)) by A15, CARD_3:9;
reconsider J = [T,g,z] as Instruction of S by A14, Def36, A4, A17;
A18: InsCode J = T by RECDEF_2:def 1;
g = JumpPart J by RECDEF_2:def 2;
hence x in JumpParts T by A18, A10; :: thesis: verum

end;

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