let S be COM-Struct ; :: thesis: for i, j being Nat
for p being NAT -defined the InstructionsF of S -valued finite Function holds Shift ((IncAddr (p,i)),j) = IncAddr ((Shift (p,j)),i)
let i, j be Nat; :: thesis: for p being NAT -defined the InstructionsF of S -valued finite Function holds Shift ((IncAddr (p,i)),j) = IncAddr ((Shift (p,j)),i)
let p be NAT -defined the InstructionsF of S -valued finite Function; :: thesis: Shift ((IncAddr (p,i)),j) = IncAddr ((Shift (p,j)),i)
set f = Shift ((IncAddr (p,i)),j);
set g = IncAddr ((Shift (p,j)),i);
dom (IncAddr (p,i)) = dom p by Def9;
then dom (Shift (p,j)) = { (m + j) where m is Nat : m in dom (IncAddr (p,i)) } by VALUED_1:def 12
.= dom (Shift ((IncAddr (p,i)),j)) by VALUED_1:def 12 ;
then A1: dom (Shift ((IncAddr (p,i)),j)) = dom (IncAddr ((Shift (p,j)),i)) by Def9;

now :: thesis: for x being object st x in dom (Shift ((IncAddr (p,i)),j)) holds
(Shift ((IncAddr (p,i)),j)) . x = (IncAddr ((Shift (p,j)),i)) . x

let x be object ; :: thesis: ( x in dom (Shift ((IncAddr (p,i)),j)) implies (Shift ((IncAddr (p,i)),j)) . x = (IncAddr ((Shift (p,j)),i)) . x )
A2: dom (Shift ((IncAddr (p,i)),j)) c= NAT by RELAT_1:def 18;
assume A3: x in dom (Shift ((IncAddr (p,i)),j)) ; :: thesis: (Shift ((IncAddr (p,i)),j)) . x = (IncAddr ((Shift (p,j)),i)) . x
then reconsider x9 = x as Element of NAT by A2;
reconsider xx = x9 as Element of NAT ;
x in { (m + j) where m is Nat : m in dom (IncAddr (p,i)) } by A3, VALUED_1:def 12;
then consider m being Nat such that
A4: x = m + j and
A5: m in dom (IncAddr (p,i)) ;
A6: m in dom p by A5, Def9;
dom (Shift (p,j)) = { (mm + j) where mm is Nat : mm in dom p } by VALUED_1:def 12;
then A7: x9 in dom (Shift (p,j)) by A4, A6;
reconsider mm = m as Element of NAT by ORDINAL1:def 12;
A8: p /. mm = p . m by A6, PARTFUN1:def 6
.= (Shift (p,j)) . (m + j) by A6, VALUED_1:def 12
.= (Shift (p,j)) /. xx by A4, A7, PARTFUN1:def 6 ;
thus (Shift ((IncAddr (p,i)),j)) . x = (IncAddr (p,i)) . m by A5, A4, VALUED_1:def 12
.= IncAddr (((Shift (p,j)) /. xx),i) by A6, A8, Def9
.= (IncAddr ((Shift (p,j)),i)) . x by A7, Def9 ; :: thesis: verum

end;

hence Shift ((IncAddr (p,i)),j) = IncAddr ((Shift (p,j)),i) by A1, FUNCT_1:2; :: thesis: verum