let k be natural number ; :: thesis: for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N
for l1, l2 being Instruction-Location of S st Start-At l1 = Start-At l2 holds
Start-At (l1 -' k) = Start-At (l2 -' k)
let N be with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N
for l1, l2 being Instruction-Location of S st Start-At l1 = Start-At l2 holds
Start-At (l1 -' k) = Start-At (l2 -' k)
let S be non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N; :: thesis: for l1, l2 being Instruction-Location of S st Start-At l1 = Start-At l2 holds
Start-At (l1 -' k) = Start-At (l2 -' k)
let l1, l2 be Instruction-Location of S; :: thesis: ( Start-At l1 = Start-At l2 implies Start-At (l1 -' k) = Start-At (l2 -' k) )
assume Start-At l1 = Start-At l2 ; :: thesis: Start-At (l1 -' k) = Start-At (l2 -' k)
then {[(IC S),l1]} = Start-At l2 by FUNCT_4:87
.= {[(IC S),l2]} by FUNCT_4:87 ;
then [(IC S),l1] = [(IC S),l2] by ZFMISC_1:6;
hence Start-At (l1 -' k) = Start-At (l2 -' k) by ZFMISC_1:33; :: thesis: verum