let i be natural number ; :: thesis: for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard-ins standard regular AMI-Struct of N
for p being NAT -defined FinPartState of holds Shift (IncAddr p,i),i = IncAddr (Shift p,i),i
let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite standard-ins standard regular AMI-Struct of N
for p being NAT -defined FinPartState of holds Shift (IncAddr p,i),i = IncAddr (Shift p,i),i
let S be non empty stored-program IC-Ins-separated definite standard-ins standard regular AMI-Struct of N; :: thesis: for p being NAT -defined FinPartState of holds Shift (IncAddr p,i),i = IncAddr (Shift p,i),i
let p be NAT -defined FinPartState of ; :: thesis: Shift (IncAddr p,i),i = IncAddr (Shift p,i),i
set f = Shift (IncAddr p,i),i;
set g = IncAddr (Shift p,i),i;
dom (IncAddr p,i) = dom p by Def15;
then dom (Shift p,i) = { (il. S,(m + i)) where m is Element of NAT : il. S,m in dom (IncAddr p,i) } by Def16
.= dom (Shift (IncAddr p,i),i) by Def16 ;
then A1: dom (Shift (IncAddr p,i),i) = dom (IncAddr (Shift p,i),i) by Def15;

now

let x be set ; :: thesis: ( x in dom (Shift (IncAddr p,i),i) implies (Shift (IncAddr p,i),i) . x = (IncAddr (Shift p,i),i) . x )
A2: dom (Shift (IncAddr p,i),i) c= NAT by RELAT_1:def 18;
assume A3: x in dom (Shift (IncAddr p,i),i) ; :: thesis: (Shift (IncAddr p,i),i) . x = (IncAddr (Shift p,i),i) . x
then reconsider x9 = x as Element of NAT by A2;
reconsider xx = x9 as Element of NAT ;
x in { (il. S,(m + i)) where m is Element of NAT : il. S,m in dom (IncAddr p,i) } by A3, Def16;
then consider m being Element of NAT such that
A4: x = il. S,(m + i) and
A5: il. S,m in dom (IncAddr p,i) ;
A6: x = (il. S,m) + i,S by A4, AMISTD_1:def 13;
A7: il. S,m in dom p by A5, Def15;
dom (Shift p,i) = { (il. S,(mm + i)) where mm is Element of NAT : il. S,mm in dom p } by Def16;
then A8: x9 in dom (Shift p,i) by A4, A7;
reconsider mm = il. S,m as Element of NAT ;
A9: pi p,mm = p . (il. S,m) by A7, AMI_1:def 47
.= (Shift p,i) . ((il. S,m) + i,S) by A7, Th65
.= (Shift p,i) . (il. S,(m + i)) by AMISTD_1:def 13
.= pi (Shift p,i),xx by A4, A8, AMI_1:def 47 ;
thus (Shift (IncAddr p,i),i) . x = (IncAddr p,i) . (il. S,m) by A5, A6, Th65
.= IncAddr (pi (Shift p,i),xx),i by A7, A9, Th74
.= (IncAddr (Shift p,i),i) . x by A8, Th74 ; :: thesis: verum

end;

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