let N be with_zero set ; :: thesis: for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for l1, l2, k being Nat holds
( Start-At ((l1 + k),S) = Start-At ((l2 + k),S) iff Start-At (l1,S) = Start-At (l2,S) )
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N; :: thesis: for l1, l2, k being Nat holds
( Start-At ((l1 + k),S) = Start-At ((l2 + k),S) iff Start-At (l1,S) = Start-At (l2,S) )
let l1, l2, k be Nat; :: thesis: ( Start-At ((l1 + k),S) = Start-At ((l2 + k),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) = Start-At ((l2 + k),S) )

assume Start-At ((l1 + k),S) = Start-At ((l2 + k),S) ; :: thesis: Start-At (l1,S) = Start-At (l2,S)
then {[(IC ),(l1 + k)]} = (IC ) .--> (l2 + k) by FUNCT_4:82;
then {[(IC ),(l1 + k)]} = {[(IC ),(l2 + k)]} by FUNCT_4:82;
then [(IC ),(l1 + k)] = [(IC ),(l2 + k)] by ZFMISC_1:3;
then l1 + k = l2 + k by XTUPLE_0:1;
hence Start-At (l1,S) = Start-At (l2,S) ; :: thesis: verum

end;

assume Start-At (l1,S) = Start-At (l2,S) ; :: thesis: Start-At ((l1 + k),S) = Start-At ((l2 + k),S)
then {[(IC ),l1]} = Start-At (l2,S) by FUNCT_4:82;
then {[(IC ),l1]} = {[(IC ),l2]} by FUNCT_4:82;
then [(IC ),l1] = [(IC ),l2] by ZFMISC_1:3;
hence Start-At ((l1 + k),S) = Start-At ((l2 + k),S) by XTUPLE_0:1; :: thesis: verum