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 ) ) )
proof
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 )
proof
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;
given g being Function such that A10: x = g and
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
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;
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 (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;
reconsider J = [T,g,z] as Element of S by A14, Def6, A19, A13;
A22: InsCode J = T ;
g = JumpPart J ;
hence x in JumpParts T by A22, 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