let f, g be Function; :: according to CARD_3:def 10 :: thesis: ( not f in JumpParts T or not g in JumpParts T or proj1 f = proj1 g )
assume f in JumpParts T ; :: thesis: ( not g in JumpParts T or proj1 f = proj1 g )
then A1: ex I being Instruction of S st
( f = JumpPart I & InsCode I = T ) ;
assume g in JumpParts T ; :: thesis: proj1 f = proj1 g
then ex J being Instruction of S st
( g = JumpPart J & InsCode J = T ) ;
hence dom f = dom g by Def33, A1; :: thesis: verum