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 A1, XTUPLE_0:def 12;

reconsider I = [T,y,z] as Element of S by A2;

A3: InsCode I = T ;

A4: JumpPart I = y ;

set f = (dom (JumpPart I)) --> NAT;

A5: dom ((dom (JumpPart I)) --> NAT) = dom (JumpPart I) 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 (JumpPart I)) --> NAT) & ( for y being object st y in dom ((dom (JumpPart I)) --> NAT) holds

g . y in ((dom (JumpPart I)) --> NAT) . y ) ) )

hence JumpParts T is product-like ; :: thesis: verum

A1: [T,y] in proj1 S by XTUPLE_0:def 12;

consider z being object such that

A2: [[T,y],z] in S by A1, XTUPLE_0:def 12;

reconsider I = [T,y,z] as Element of S by A2;

A3: InsCode I = T ;

A4: JumpPart I = y ;

set f = (dom (JumpPart I)) --> NAT;

A5: dom ((dom (JumpPart I)) --> NAT) = dom (JumpPart I) 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 (JumpPart I)) --> NAT) & ( for y being object st y in dom ((dom (JumpPart I)) --> NAT) holds

g . y in ((dom (JumpPart I)) --> NAT) . y ) ) )

proof

then
JumpParts T = product ((dom (JumpPart I)) --> NAT)
by CARD_3:def 5;
let x be object ; :: thesis: ( x in JumpParts T iff ex g being Function st

( x = g & dom g = dom ((dom (JumpPart I)) --> NAT) & ( for y being object 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 object 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 object st y in dom ((dom (JumpPart I)) --> NAT) holds

g . y in ((dom (JumpPart I)) --> NAT) . y ) ) implies x in JumpParts T )

A11: dom g = dom ((dom (JumpPart I)) --> NAT) and

A12: for y being object 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, CARD_3:100;

A16: for x being object st x in dom (product" (JumpParts T)) holds

g . x in (product" (JumpParts T)) . x

A22: InsCode J = T ;

g = JumpPart J ;

hence x in JumpParts T by A22, A10; :: thesis: verum

end;( x = g & dom g = dom ((dom (JumpPart I)) --> NAT) & ( for y being object 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 object 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 object st y in dom ((dom (JumpPart I)) --> NAT) holds

g . y in ((dom (JumpPart I)) --> NAT) . y ) ) implies x in JumpParts T )

proof

given g being Function such that A10:
x = g
and
assume
x in JumpParts T
; :: thesis: ex g being Function st

( x = g & dom g = dom ((dom (JumpPart I)) --> NAT) & ( for y being object st y in dom ((dom (JumpPart I)) --> NAT) holds

g . y in ((dom (JumpPart I)) --> 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 (JumpPart I)) --> NAT) & ( for y being object 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 object 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, Def5, A5; :: thesis: for y being object st y in dom ((dom (JumpPart I)) --> NAT) holds

g . y in ((dom (JumpPart I)) --> NAT) . y

let y be object ; :: 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;( x = g & dom g = dom ((dom (JumpPart I)) --> NAT) & ( for y being object st y in dom ((dom (JumpPart I)) --> NAT) holds

g . y in ((dom (JumpPart I)) --> 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 (JumpPart I)) --> NAT) & ( for y being object 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 object 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, Def5, A5; :: thesis: for y being object st y in dom ((dom (JumpPart I)) --> NAT) holds

g . y in ((dom (JumpPart I)) --> NAT) . y

let y be object ; :: 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

A11: dom g = dom ((dom (JumpPart I)) --> NAT) and

A12: for y being object 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, CARD_3:100;

A16: for x being object st x in dom (product" (JumpParts T)) holds

g . x in (product" (JumpParts T)) . x

proof

A19:
g is natural-valued
let x be object ; :: thesis: ( x in dom (product" (JumpParts T)) implies g . x in (product" (JumpParts T)) . x )

assume A17: x in dom (product" (JumpParts T)) ; :: thesis: g . x in (product" (JumpParts T)) . x

A18: NAT c= (product" (JumpParts (InsCode I))) . x by A17, A15, A13, Lm3;

((dom (JumpPart I)) --> NAT) . x = NAT by A15, A13, A17, FUNCOP_1:7;

then g . x in NAT by A12, A15, A17, A11;

hence g . x in (product" (JumpParts T)) . x by A18; :: thesis: verum

end;assume A17: x in dom (product" (JumpParts T)) ; :: thesis: g . x in (product" (JumpParts T)) . x

A18: NAT c= (product" (JumpParts (InsCode I))) . x by A17, A15, A13, Lm3;

((dom (JumpPart I)) --> NAT) . x = NAT by A15, A13, A17, FUNCOP_1:7;

then g . x in NAT by A12, A15, A17, A11;

hence g . x in (product" (JumpParts T)) . x by A18; :: thesis: verum

proof

reconsider J = [T,g,z] as Element of S by A14, Def6, A19, A13;
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 (InsCode I))) . x c= NAT by Lm2, A13;

g . x in (product" (JumpParts T)) . x by A15, A16, A20;

hence g . x is natural by A21; :: thesis: verum

end;assume A20: x in dom g ; :: thesis: g . x is natural

then A21: (product" (JumpParts (InsCode I))) . x c= NAT by Lm2, A13;

g . x in (product" (JumpParts T)) . x by A15, A16, A20;

hence g . x is natural by A21; :: thesis: verum

A22: InsCode J = T ;

g = JumpPart J ;

hence x in JumpParts T by A22, A10; :: thesis: verum

hence JumpParts T is product-like ; :: thesis: verum