let i, j be Element of SCMPDS-Instr ; :: according to COMPOS_0:def 5 :: thesis: ( not InsCode i = InsCode j or dom (JumpPart i) = dom (JumpPart j) )
assume A1: InsCode i = InsCode j ; :: thesis: dom (JumpPart i) = dom (JumpPart j)
not not InsCode i = 0 & ... & not InsCode i = 14 by Lm2, NAT_1:60;

per cases then ( InsCode i = 0 or InsCode i = 14 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 or InsCode i = 8 or InsCode i = 9 or InsCode i = 10 or InsCode i = 11 or InsCode i = 12 or InsCode i = 13 ) ;

suppose InsCode i = 0 ; :: thesis: dom (JumpPart i) = dom (JumpPart j)

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

end;

suppose InsCode i = 14 ; :: thesis: dom (JumpPart i) = dom (JumpPart j)

then ( JumpPart i = {} & JumpPart j = {} ) by A1, Lm4;
hence dom (JumpPart i) = dom (JumpPart j) ; :: thesis: verum

end;

suppose InsCode i = 1 ; :: thesis: dom (JumpPart i) = dom (JumpPart j)

then ( JumpPart i = {} & JumpPart j = {} ) by A1, Lm5;
hence dom (JumpPart i) = dom (JumpPart j) ; :: thesis: verum

end;

suppose ( InsCode i = 2 or InsCode i = 3 ) ; :: thesis: dom (JumpPart i) = dom (JumpPart j)

then ( JumpPart i = {} & JumpPart j = {} ) by A1, Lm6;
hence dom (JumpPart i) = dom (JumpPart j) ; :: thesis: verum

end;

suppose ( InsCode i = 4 or InsCode i = 5 or InsCode i = 6 or InsCode i = 7 or InsCode i = 8 ) ; :: thesis: dom (JumpPart i) = dom (JumpPart j)

then ( JumpPart i = {} & JumpPart j = {} ) by A1, Lm7;
hence dom (JumpPart i) = dom (JumpPart j) ; :: thesis: verum

end;

suppose ( InsCode i = 9 or InsCode i = 10 or InsCode i = 11 or InsCode i = 12 or InsCode i = 13 ) ; :: thesis: dom (JumpPart i) = dom (JumpPart j)

then ( JumpPart i = {} & JumpPart j = {} ) by A1, Lm8;
hence dom (JumpPart i) = dom (JumpPart j) ; :: thesis: verum

end;

end;