let i be Element of NAT ; :: thesis: for p being NAT -defined the Instructions of SCM -valued finite Function holds Shift ((IncAddr (p,i)),i) = Reloc (p,i)
let p be NAT -defined the Instructions of SCM -valued finite Function; :: thesis: Shift ((IncAddr (p,i)),i) = Reloc (p,i)
dom (IncAddr (p,i)) = dom p by COMPOS_1:def 40;
then A1: dom (Shift (p,i)) = { (m + i) where m is Element of NAT : m in dom (IncAddr (p,i)) } by VALUED_1:def 12
.= dom (Shift ((IncAddr (p,i)),i)) by VALUED_1:def 12 ;

A2: now

let x be set ; :: thesis: ( x in dom (Shift ((IncAddr (p,i)),i)) implies (Shift ((IncAddr (p,i)),i)) . x = (Reloc (p,i)) . x )
assume A3: x in dom (Shift ((IncAddr (p,i)),i)) ; :: thesis: (Shift ((IncAddr (p,i)),i)) . x = (Reloc (p,i)) . x
then A4: x in { (m + i) where m is Element of NAT : m in dom (IncAddr (p,i)) } by VALUED_1:def 12;
dom (Shift ((IncAddr (p,i)),i)) c= NAT by RELAT_1:def 18;
then reconsider x9 = x as Element of NAT by A3;
consider m being Element of NAT such that
A5: x = m + i and
A6: m in dom (IncAddr (p,i)) by A4;
A7: m in dom p by A6, COMPOS_1:def 40;
dom (Shift (p,i)) = { (mm + i) where mm is Element of NAT : mm in dom p } by VALUED_1:def 12;
then A8: x9 in dom (Shift (p,i)) by A5, A7;
A9: p /. m = p . m by A7, PARTFUN1:def 8
.= (Shift (p,i)) . (m + i) by A7, VALUED_1:def 12
.= (Shift (p,i)) /. x9 by A5, A8, PARTFUN1:def 8 ;
thus (Shift ((IncAddr (p,i)),i)) . x = (IncAddr (p,i)) . m by A5, A6, VALUED_1:def 12
.= IncAddr (((Shift (p,i)) /. x9),i) by A7, A9, COMPOS_1:def 40
.= (Reloc (p,i)) . x by A8, COMPOS_1:def 40 ; :: thesis: verum

end;

dom (Reloc (p,i)) = dom (Shift (p,i)) by COMPOS_1:def 40;
hence Shift ((IncAddr (p,i)),i) = Reloc (p,i) by A1, A2, FUNCT_1:9; :: thesis: verum