let N be with_non-empty_elements set ; :: thesis: for S being non empty IC-Ins-separated AMI-Struct of NAT ,N
for l1, l2 being Instruction-Location of S
for k being Element of NAT holds
( Start-At (l1 + k) = Start-At (l2 + k) iff Start-At l1 = Start-At l2 )
let S be non empty IC-Ins-separated AMI-Struct of NAT ,N; :: thesis: for l1, l2 being Instruction-Location of S
for k being Element of NAT holds
( Start-At (l1 + k) = Start-At (l2 + k) iff Start-At l1 = Start-At l2 )
let l1, l2 be Instruction-Location of S; :: thesis: for k being Element of NAT holds
( Start-At (l1 + k) = Start-At (l2 + k) iff Start-At l1 = Start-At l2 )
let k be Element of NAT ; :: thesis: ( Start-At (l1 + k) = Start-At (l2 + k) iff Start-At l1 = Start-At l2 )

hereby :: thesis: ( Start-At l1 = Start-At l2 implies Start-At (l1 + k) = Start-At (l2 + k) )

assume A1: Start-At (l1 + k) = Start-At (l2 + k) ; :: thesis: Start-At l1 = Start-At l2
{[(IC S),(l1 + k)]} = (IC S) .--> (l2 + k) by A1, FUNCT_4:87;
then {[(IC S),(l1 + k)]} = {[(IC S),(l2 + k)]} by FUNCT_4:87;
then [(IC S),(l1 + k)] = [(IC S),(l2 + k)] by ZFMISC_1:6;
then l1 + k = l2 + k by ZFMISC_1:33;
hence Start-At l1 = Start-At l2 ; :: thesis: verum

end;

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;
then {[(IC S),l1]} = {[(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