theorem Th22: :: COMPOS_1:34

for S being COM-Struct
for i, j being Nat
for p being NAT -defined the InstructionsF of b₁ -valued finite Function holds Shift ((IncAddr (p,i)),j) = IncAddr ((Shift (p,j)),i)