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