let N be set ; :: thesis: for S being standard-ins COM-Struct of N
for I, J being Instruction of S st InsCode I = InsCode J & JumpPart I = JumpPart J & AddressPart I = AddressPart J holds
I = J
let S be standard-ins COM-Struct of N; :: thesis: for I, J being Instruction of S st InsCode I = InsCode J & JumpPart I = JumpPart J & AddressPart I = AddressPart J holds
I = J
let I, J be Instruction 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
W: the Instructions of S c= [:NAT,(NAT *),(X *):] by Def17;
I in the Instructions of S ;
then Y: I in [:NAT,(NAT *),(X *):] by W;
J in the Instructions of S ;
then J in [:NAT,(NAT *),(X *):] by W;
hence ( InsCode I = InsCode J & JumpPart I = JumpPart J & AddressPart I = AddressPart J implies I = J ) by Y, RECDEF_2:10; :: thesis: verum