consider y being object such that
A1: [T,y] in proj1 S by XTUPLE_0:def 12;
consider x being object such that
A2: [[T,y],x] in S by A1, XTUPLE_0:def 12;
reconsider I = [T,y,x] as Element of S by A2;
InsCode I = T ;
then JumpPart I in JumpParts T ;
hence not JumpParts T is empty ; :: thesis: JumpParts T is functional
let f be object ; :: according to FUNCT_1:def 13 :: thesis: ( not f in JumpParts T or f is set )
assume f in JumpParts T ; :: thesis: f is set
then ex I being Element of S st
( f = JumpPart I & InsCode I = T ) ;
hence f is set ; :: thesis: verum