let k 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 AMI-Struct of N
for l1, l2 being Element of NAT holds
( Start-At (l1 + k,S),S = Start-At (l2 + k,S),S iff Start-At l1,S = Start-At l2,S )
let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite standard AMI-Struct of N
for l1, l2 being Element of NAT holds
( Start-At (l1 + k,S),S = Start-At (l2 + k,S),S iff Start-At l1,S = Start-At l2,S )
let S be non empty stored-program IC-Ins-separated definite standard AMI-Struct of N; :: thesis: for l1, l2 being Element of NAT holds
( Start-At (l1 + k,S),S = Start-At (l2 + k,S),S iff Start-At l1,S = Start-At l2,S )
let l1, l2 be Element of NAT ; :: thesis: ( Start-At (l1 + k,S),S = Start-At (l2 + k,S),S iff Start-At l1,S = Start-At l2,S )

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

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

end;

assume Start-At l1,S = Start-At l2,S ; :: thesis: Start-At (l1 + k,S),S = Start-At (l2 + k,S),S
then {[(IC S),l1]} = Start-At l2,S 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,S),S = Start-At (l2 + k,S),S by ZFMISC_1:33; :: thesis: verum