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 that

A1: f in JumpParts T and

A2: g in JumpParts T ; :: thesis: proj1 f = proj1 g

A3: ex I being Element of S st

( f = JumpPart I & InsCode I = T ) by A1;

ex J being Element of S st

( g = JumpPart J & InsCode J = T ) by A2;

hence proj1 f = proj1 g by A3, Def5; :: thesis: verum

assume that

A1: f in JumpParts T and

A2: g in JumpParts T ; :: thesis: proj1 f = proj1 g

A3: ex I being Element of S st

( f = JumpPart I & InsCode I = T ) by A1;

ex J being Element of S st

( g = JumpPart J & InsCode J = T ) by A2;

hence proj1 f = proj1 g by A3, Def5; :: thesis: verum