consider y being set such that
A1: [T,y] in proj1 the Instructions of S by RELAT_1:def 4;
consider x being set such that
A2: [[T,y],x] in the Instructions of S by A1, RELAT_1:def 4;
reconsider I = [T,y,x] as Instruction of S by A2;
InsCode I = T by RECDEF_2:def 1;
then JumpPart I in JumpParts T ;
hence not JumpParts T is empty ; :: thesis: JumpParts T is functional
let f be set ; :: 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 Instruction of S st
( f = JumpPart I & InsCode I = T ) ;
hence f is set ; :: thesis: verum