let II, I be Instruction of SCM; :: thesis: for k being Element of NAT st not not InsCode I = 0 & ... & not InsCode I = 5 & IncAddr (II,k) = I holds
II = I
let k be Element of NAT ; :: thesis: ( not not InsCode I = 0 & ... & not InsCode I = 5 & IncAddr (II,k) = I implies II = I )
assume that
A1: not not InsCode I = 0 & ... & not InsCode I = 5 and
A2: IncAddr (II,k) = I ; :: thesis: II = I
IncAddr (I,k) = I by A1, Th4;
hence II = I by A2, COMPOS_0:6; :: thesis: verum