let i, j be Element of SCM-Instr R; :: according to COMPOS_0:def 5 :: thesis: ( not InsCode i = InsCode j or dom (i `2_3) = dom (j `2_3) )
assume A1: InsCode i = InsCode j ; :: thesis: dom (i `2_3) = dom (j `2_3)
InsCode i <= 7 by Lm1;

per cases then ( InsCode i = 0 or InsCode i = 1 or InsCode i = 2 or InsCode i = 3 or InsCode i = 4 or InsCode i = 5 or InsCode i = 6 or InsCode i = 7 ) by NAT_1:31;

suppose InsCode i = 0 ; :: thesis: dom (i `2_3) = dom (j `2_3)

then ( i in {[0,{},{}]} & j in {[0,{},{}]} ) by A1, Th7;
then ( i = [0,{},{}] & j = [0,{},{}] ) by TARSKI:def 1;
hence dom (i `2_3) = dom (j `2_3) ; :: thesis: verum

end;

suppose ( InsCode i = 1 or InsCode i = 2 or InsCode i = 3 or InsCode i = 4 ) ; :: thesis: dom (i `2_3) = dom (j `2_3)

then ( JumpPart i = {} & JumpPart j = {} ) by A1, Lm2;
hence dom (i `2_3) = dom (j `2_3) ; :: thesis: verum

end;

suppose InsCode i = 5 ; :: thesis: dom (i `2_3) = dom (j `2_3)

then ( JumpPart i = {} & JumpPart j = {} ) by A1, Lm3;
hence dom (i `2_3) = dom (j `2_3) ; :: thesis: verum

end;

suppose InsCode i = 6 ; :: thesis: dom (i `2_3) = dom (j `2_3)

then ( dom (JumpPart i) = Seg 1 & dom (JumpPart j) = Seg 1 ) by A1, Lm4;
hence dom (i `2_3) = dom (j `2_3) ; :: thesis: verum

end;

suppose InsCode i = 7 ; :: thesis: dom (i `2_3) = dom (j `2_3)

then ( dom (JumpPart i) = Seg 1 & dom (JumpPart j) = Seg 1 ) by A1, Lm5;
hence dom (i `2_3) = dom (j `2_3) ; :: thesis: verum

end;

end;