let S be non empty standard-ins set ; :: thesis: for I, J being Element of S st InsCode I = InsCode J & JumpPart I = JumpPart J & AddressPart I = AddressPart J holds

I = J

let I, J be Element of S; :: thesis: ( InsCode I = InsCode J & JumpPart I = JumpPart J & AddressPart I = AddressPart J implies I = J )

consider X being non empty set such that

A1: S c= [:NAT,(NAT *),(X *):] by Def1;

A2: I in S ;

J in S ;

hence ( InsCode I = InsCode J & JumpPart I = JumpPart J & AddressPart I = AddressPart J implies I = J ) by A2, A1, RECDEF_2:10; :: thesis: verum

I = J

let I, J be Element of S; :: thesis: ( InsCode I = InsCode J & JumpPart I = JumpPart J & AddressPart I = AddressPart J implies I = J )

consider X being non empty set such that

A1: S c= [:NAT,(NAT *),(X *):] by Def1;

A2: I in S ;

J in S ;

hence ( InsCode I = InsCode J & JumpPart I = JumpPart J & AddressPart I = AddressPart J implies I = J ) by A2, A1, RECDEF_2:10; :: thesis: verum