consider y being object such that
A1: [T,y] in proj1 S by XTUPLE_0:def 12;
consider z being object such that
A2: [[T,y],z] in S by ;
reconsider I = [T,y,z] as Element of S by A2;
A3: InsCode I = T ;
A4: JumpPart I = y ;
set f = (dom ()) --> NAT;
A5: dom ((dom ()) --> NAT) = dom () by FUNCOP_1:13;
for x being object holds
( x in JumpParts T iff ex g being Function st
( x = g & dom g = dom ((dom ()) --> NAT) & ( for y being object st y in dom ((dom ()) --> NAT) holds
g . y in ((dom ()) --> NAT) . y ) ) )
proof
let x be object ; :: thesis: ( x in JumpParts T iff ex g being Function st
( x = g & dom g = dom ((dom ()) --> NAT) & ( for y being object st y in dom ((dom ()) --> NAT) holds
g . y in ((dom ()) --> NAT) . y ) ) )

thus ( x in JumpParts T implies ex g being Function st
( x = g & dom g = dom ((dom ()) --> NAT) & ( for y being object st y in dom ((dom ()) --> NAT) holds
g . y in ((dom ()) --> NAT) . y ) ) ) :: thesis: ( ex g being Function st
( x = g & dom g = dom ((dom ()) --> NAT) & ( for y being object st y in dom ((dom ()) --> NAT) holds
g . y in ((dom ()) --> 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 ()) --> NAT) & ( for y being object st y in dom ((dom ()) --> NAT) holds
g . y in ((dom ()) --> NAT) . y ) )

then consider K being Element of S such that
A6: x = JumpPart K and
A7: InsCode K = T ;
take g = JumpPart K; :: thesis: ( x = g & dom g = dom ((dom ()) --> NAT) & ( for y being object st y in dom ((dom ()) --> NAT) holds
g . y in ((dom ()) --> NAT) . y ) )

thus x = g by A6; :: thesis: ( dom g = dom ((dom ()) --> NAT) & ( for y being object st y in dom ((dom ()) --> NAT) holds
g . y in ((dom ()) --> NAT) . y ) )

thus A8: dom g = dom ((dom ()) --> NAT) by A7, A3, Def5, A5; :: thesis: for y being object st y in dom ((dom ()) --> NAT) holds
g . y in ((dom ()) --> NAT) . y

let y be object ; :: thesis: ( y in dom ((dom ()) --> NAT) implies g . y in ((dom ()) --> NAT) . y )
assume A9: y in dom ((dom ()) --> NAT) ; :: thesis: g . y in ((dom ()) --> NAT) . y
then ((dom ()) --> NAT) . y = NAT by ;
hence g . y in ((dom ()) --> NAT) . y by ; :: thesis: verum
end;
given g being Function such that A10: x = g and
A11: dom g = dom ((dom ()) --> NAT) and
A12: for y being object st y in dom ((dom ()) --> NAT) holds
g . y in ((dom ()) --> NAT) . y ; :: thesis:
A13: dom g = dom () by ;
set J = [T,g,z];
A14: y in JumpParts T by A4, A3;
then A15: dom g = dom () by ;
A16: for x being object st x in dom () holds
g . x in () . x
proof
let x be object ; :: thesis: ( x in dom () implies g . x in () . x )
assume A17: x in dom () ; :: thesis: g . x in () . x
A18: NAT c= (product" (JumpParts ())) . x by A17, A15, A13, Lm3;
((dom ()) --> NAT) . x = NAT by ;
then g . x in NAT by A12, A15, A17, A11;
hence g . x in () . x by A18; :: thesis: verum
end;
A19: g is natural-valued
proof
let x be object ; :: according to VALUED_0:def 12 :: thesis: ( not x in proj1 g or g . x is natural )
assume A20: x in dom g ; :: thesis: g . x is natural
then A21: (product" (JumpParts ())) . x c= NAT by ;
g . x in () . x by ;
hence g . x is natural by A21; :: thesis: verum
end;
reconsider J = [T,g,z] as Element of S by ;
A22: InsCode J = T ;
g = JumpPart J ;
hence x in JumpParts T by ; :: thesis: verum
end;
then JumpParts T = product ((dom ()) --> NAT) by CARD_3:def 5;
hence JumpParts T is product-like ; :: thesis: verum