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

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